I have been wondering for a couple of years who will be the first in the race to set up a a publicly available, working and usable formalized math wiki. Now ladies and gentlemen we have the winner and the winner is Wikiproofs.org!
I am not actually completely sure that this is the first one. It has been online since June 2009 and I didn’t know about it, so it is quite possible that I missed some other one as well. Please tell me if this is the case. But for now I consider it the first ever.
Some of my hopes/predictions turned to be accurate. The wiki is not affiliated with any research institution. It is not financed by an EU grant, or any other taxpayer’s money redistribution mechanism. It does not promise to allow writing software that is free of bugs. It did not announce its existence to the world before it existed. Not that there would be anything wrong with all that, just that I didn’t consider it likely for a project that does any of this to succeed.
The proofs are verified with JHilbert, written in Java by Alexander Klauer. JHilbert has been influenced by Metamath, although its language is different.
There are a lot of things that I like about Wikiproofs. JHilbert is of Metamath descent and that means it is very generic. There are modules formulating ZFC axioms of course, but there also things like geometry and complex numbers axioms. This brings memories from high school when I learned geometry by the axiomatic method (and vice versa). The wiki uses my favorite style of interleaving the formal text with informal commentary, taking it a step farther than what I do in IsarMathLib by putting comments also inside proofs, not only between theorems. With MediaWiki one can illustrate geometry proofs with pictures.
So, will I contribute to wikiproofs.org? Six years ago I would definitely answer yes. Now, however, the answer is “probably not yet”. After years of writing Isar proofs I have a clear view on what I need for fun proving:
1) I need a high-level language for structured proofs with automation at least on the level provided by Isabelle/Isar. Writing formal proofs is tedious and Metamath-style proofs are beyond of what I can bear. Creating a Metamath prover (rather than checker) that would allow to take larger steps in the proofs is apparently a very difficult problem that nobody has been able to solve so far (am I wrong here?).
2) I need a readable presentation for my proofs so that I can hope they can be studied by someone who does not know the formal proof language. “Readable” here means just that: close enough to standard (informal) proofs that a person who can follow a detailed informal proof can follow also the formalized version of it without having first to study the proof language. This gives me some justification in my own eyes of spending endless hours of crafting a formal proof of something that is proven by “clearly” keyword in the informal math. Wikiproofs may some day have a more friendly presentation layer for formal text, I think there are no fundamental obstacles here.