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.

Screenshot:

Publications:

MKM'07: (with P. Corbineau) Cooperative repositories for formal proofs - A Wiki based solution, LNCS (pdf, bib)
SemWiki'08: (coauthored) A real Semantic Web for mathematics deserves a real semantics, Coeur-ws (pdf, bib)

All pdfs provided above are preprints.

Presentations about MathWiki:

ICIS colloquium, Nijmegen (28/4/2008) (pdf slides)
MathWiki Workshop, Edinburgh (Nov 2007) (pdf slides)
SemWiki workshop (pdf slides)
PGIP Implementers meeting, Munich (Mar 2007) (pdf slides)
Chat Types workshop (Dec 2006) (pdf slides)

Final product:

We imagine the final product to:

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

We imagine it to look like:

Workshop

In 2007, there was a Types MathWiki workshop which gathered people willing to work on a wiki for formalized mathematics. 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
INRIA
Uniwersytet w Białymstoku
Jacobs University Bremen