Wiki for formalized mathematics based on ProofWeb
- Prototype based on MediaWiki.
- It currently supports only Coq (and is quite buggy)
(ProofWeb works with many provers; Isabelle, Lego, Plastic, Matita, ...)
- Uses the ProofWeb interface to interactively interact with the proof assistant.
- All links are clickable and pages editable (AJAX interface resembling CoqIde).
- Informal mathematics in comments can use LaTeX which is rendered on the server.
- Dependencides between files are calculated in a dynamic way.
- Look at the MKM conference publication for more info (pdf).
It works, but since it is very buggy we do not link it from here. If you would like to
try it, please contact us.
All pdfs provided above are preprints.
- (with P. Corbineau) Cooperative repositories for formal proofs - A Wiki based solution, LNCS
- (coauthored) A real Semantic Web for mathematics deserves a real semantics, Coeur-ws
Presentations about MathWiki:
We imagine the final product to:
We imagine it to look like:
- Fully support scripts in multiple proof assistants
- Include semantic annotations
- Combine with HELM / WHELP
- Provide syntax highliting also during edition
- Use Unicode in proofs and not only in comments
- Allow more browser sessions editing the same file
In 2007, there was a Types MathWiki
workshop which gathered people willing to work on a wiki for formalized
The people who expressed interest in collaborating about creating
a common Wiki for formalized mathematics, with whom we plan to work:
- Radboud Universiteit Nijmegen
- Università di Bologna
- University of Edinburgh
- Technische Universität München
- Uniwersytet w Białymstoku
- Jacobs University Bremen