An integrated web platform for the Mizar Mathematical Library

DOI10.1007/978-3-031-16681-5_9MaRDI QIDQ6159377zbMATH OpenOpenAlexFDO

Authors Hideharu Furushima, Daichi Yamamichi, Seigo Shigenaka, Kazuhisa Nakasho, Katsumi Wasaki

Publication date 2 June 2023

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2210.02336

zbMATH Keywords

mathematical knowledge managementMizar Mathematical LibraryQED manifestoweb service

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Abstract: This paper reports on the development of a Web platform to host the Mizar Mathematical Library (MML). In recent years, the size of formalized mathematical libraries has been drastically increasing, and this has led to a growing demand for tools that support efficient and comprehensive browsing, searching, and annotation of these libraries. This platform implements a Wiki function to add comments to the HTMLized MML, three types of search function (article, symbol, and theorem), and a function to show the dependency graph of the MML. This platform is designed with consistency, scalability, and interoperability as top priorities for long-term use.

Recommendations

• The role of the Mizar mathematical library for interactive proof development in Mizar
• System description: MathHub.info
• Mathematical Knowledge Management
• scientific article; zbMATH DE number 1951637
• scientific article; zbMATH DE number 1951634

Cites work

• A Wiki for Mizar: motivation, considerations, and initial prototype
• ATP and presentation service for Mizar formalizations
• Dependencies in formal mathematics: applications and extraction for Coq and Mizar
• Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
• Formal mathematics on display: a wiki for Flyspeck
• Four decades of \textsc{Mizar}. Foreword
• scientific article; zbMATH DE number 1951634 (Why is no real title available?)
• Integrating searching and authoring in Mizar
• Large formal wikis: issues and solutions
• Maintaining a library of formal mathematics
• Mathematical knowledge management in MIZAR
• MathJax: a platform for mathematics on the web
• mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
• TGView3D: a system for 3-dimensional visualization of theory graphs
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Tools for MML environment analysis

Cited in

(4)

• WebMIaS on Docker. Deploying math-aware search in a single line of code
• Re-imagining the Isabelle archive of formal proofs
• Remote verification system for Mizar integrated with emwiki
• Exploring formal math on the blockchain: an explorer for Proofgold

This page was built for publication: An integrated web platform for the Mizar Mathematical Library

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6159377)