MathWiki

What?

• This is an NWO-funded project to put formal mathematics into a wiki.

Who?

The core project group is the Foundations Group at RU Nijmegen, however the project welcomes collaboration from anybody anywhere. The current contributors are:

People at RU:

• Herman Geuvers (project leader)

• Kasper Brink

• James McKinna

• Lionel Mamane

• Sebastian Reichelt

• Carst Tankink

• Josef Urban

• Freek Wiedijk

People outside RU:

• Jesse Alama (CENTRIA, Lisboa)

• Cezary Kaliszyk (University of Tsukuba)

• Piotr Rudnicki (Department of Computing Science, University of Alberta)

Background to the Research

We believe that formal (computer understandable and verifiable) mathematics has many advantages and is inevitable in the long term. Formal mathematics is not only important because it allows unmatched precision in checking the validity of (sometimes extremely long and complex) important ideas and designs. It is also important as a field providing uniquely deep understanding between computers and humans, allowing them to cooperate on semantic level in a number of novel strong ways that cannot be found in other areas.

There can obviously be various ideas about how formal mathematical wikis should look and what kind of functionality they should provide. For example, they could be just tools for collaborative web-based editing and development of existing formal libraries, or they could also provide a number of functions helping with formalization and understanding of formal mathematical texts and libraries. The wikis could target the existing systems and developers of formal libraries, or they could focus more on making formalization accessible to outsiders. Ideally, our efforts should lead to a platform and tools that make (collaborative) formalization much easier and smoother than it is today for everybody interested, and that allow development of large re-usable formal repositories analogous to the informal Wikipedia and Planetmath repositories.

The Basis

A starting point for the project are existing formal systems with large libraries, and the tools available for them. The current group's expertise is mainly in the Coq and Mizar systems. However the issues we are solving are to a large extent system-independent and we hope to make our techniques available for other major formal systems like Isabelle , HOL , HOL Light , and others. Our manpower is however limited, so anybody interested in collaboration is welcome.

The Tasks

Our focus so far has been on the following (high-level) tasks:

• Developing a suitable backend model for the wiki. This should allow both (one-file) web-based editing (and verification) and also large (many-file) operations using standard (distributed) version control access to the wiki. We work mostly with git (being inspired by Ikiwiki), but would like to include also Mercurial (used by Isabelle developers).

• Instantiating and testing this model for Mizar/MML and Coq/CORN systems and libraries.

• Providing suitable rich HTML presentations for the libraries. This is a novel work on proof movies (currently for Coq and Isabelle), and continuous work on HTML presentation of Mizar.

• Providing suitable common cross-linking layer (based likely on Wikipedia annotations) for different systems/libraries.

• Providing a number of tools for strong formalization support in the web setting. This is currently being done for Mizar, using the link to external ATP systems and machine learning advisors.

• Providing detailed dependency analysis and tools (allowing smart/fast recompilation and refactoring) for at least some of the systems (Mizar, Coq). This is harder than it may seem, especially in the context of established proof assistants.

• Especially in case of Mizar/MML, a necessary part is developing proper licensing for publicly developed libraries of formal mathematics.

• We maintain the ProofWeb web interface to Coq and other proof assistants written by Cezary Kaliszyk, and intend to integrate it (or a modified version) with our backend(s), again, possibly adding to it a number of support tools.

• Check our MathWikiDevel development page for more (not necessarily up-to-date) plans, details, and ideas.

The Results

Our current prototypes/systems/proposals and software developed so far are:

• The git-based Mizar/MML wiki and Coq/CORN wiki. Note that these are rapidly moving targets (however we have some bold users already). The code is at https://github.com/JUrban/mwiki , https://github.com/jessealama/mwiki and http://bitbucket.org/Carst/mathwiki .

• Proviola is a tool for creating dynamic (HTML + Javascript) pages out of proof scripts, allowing readers to zip through a proof. The code is at http://bitbucket.org/Carst/proviola-source .

• The Mizar HTML-ization code is developed at https://github.com/JUrban/xsl4mizar .

• The Automated Reasoning for Mizar system integrating strong ATP/AI tools with Mizar verification and web presentation. The code is available at https://github.com/JUrban/MPTP2/tree/master/MizAR/ .

• Isabelle XML RPC uses Isabelle's Scala wrapper (developed by Makarius Wenzel) to export the prover's functionality over the Web. This functionality is used to make movies out of Isabelle scripts. The code is at http://bitbucket.org/Carst/isabelle_xmlrpc

• The ProofWeb web interface by Cezary Kaliszyk, downloadable at http://prover.cs.ru.nl/install.php .

• The MML licensing proposal (now accepted by the Association of Mizar Users as of Oct 28 2010) is at https://github.com/JUrban/MMLLicense .

Publications

• Jesse Alama, Kasper Brink, Lionel Mamane, Josef Urban: Large Formal Wikis: Issues and Solutions. Calculemus/MKM 2011: 133-148

• Carst Tankink, James McKinna: Dynamic Proof Pages, MathWikis 2011: 45-48

• Sebastian Reichelt: Ideas for a MathWiki Editor, MathWikis 2011: 38-44

• Josef Urban: Content-based encoding of mathematical and code libraries, MathWikis 2011: 49-53

• Jesse Alama: Metadata for a wiki of formalized mathematics, MathWikis 2011: 2-5

• Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, Josef Urban: Licensing the Mizar Mathematical Library. Calculemus/MKM 2011: 149-163

• Josef Urban, Jesse Alama, Piotr Rudnicki, Herman Geuvers: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. AISC/MKM/Calculemus 2010: 455-469

• Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk: Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus 2010: 440-454

• Josef Urban, Geoff Sutcliffe: Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. AISC/MKM/Calculemus 2010: 132-146

• Carst Tankink, Herman Geuvers, and James McKinna. Narrating formal proof (work in progress). In David Aspinall and Claudio Sacerdoti Coen, editors, User Interfaces for Theorem Provers 2010. To appear in an issue of ENTCS, 2010.

• Josef Urban, Krystof Hoder, Andrei Voronkov: Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS 2010: 155-166

• Jiri Vyskocil, David Stanovsky, Josef Urban: Automated proof compression by invention of new definitions, LPAR-16 (Dakar, 2010), in LNAI 6355.