The first formalized math wiki is here

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.

Advertisements

Tags: ,

4 Responses to “The first formalized math wiki is here”

  1. Jesse Alama Says:

    There’s been a wiki for Mizar since early 2010 at http://mws.cs.ru.nl/mwik. It’s recently been extended to deal with part of Coq, and sports a number of features.

  2. Alexander Klauer Says:

    Hello, I stumbled over this here blog entry. First off, thanks for all the praise. Allow me to add some more info about Wikiproofs, in order to avoid misconceptions.

    It’s true that Wikiproofs has been online since 1 June 2009. However, I registered the domain wikiproofs.org only on 1 September 2010. Before that date, Wikiproofs was (and still is) available under wikiproofs.de. Back in 2009, the domain wikiproofs.org was unavailable. Before 2009, I’ve been searching the net a lot for something like a formal proof wiki. I found a lot of interesting projects (qedeq, Mizar, metamath, just to name some) but not a true wiki. Had I found one, wikiproofs.org would probably not exist today, but here it is, and it really seems like it’s the first one.

    It’s also true that JHilbert is influenced by metamath. That’s because JHilbert is based on Ghilbert by Raph Levien. The JHilbert language and most of the internal mechanisms of JHilbert are essentially due to Raph’s. I wrote JHilbert at a time when it looked like Raph had abandoned development of Ghilbert (it turned out he hadn’t).

    As for the current Wiki content, I provided only a small part of it. The lion’s share of content has been added by user Kingdon. Without him, Wikiproofs would be quite an empty place today.

    Wikiproofs is still in the infant stage and I’ve got a lot of plans for further improvement. Sadly, I also seem to find very little time to invest in the development of Wikiproofs at the moment, with no improvement in sight (I’ve got a thesis defence coming up, and soon after I’ll probably be working in some job outside academia).

    But do feel free to play around with the site (remember that you can also use JHilbert as a command line tool) or even participate in development. Some source code is available at GitHub.

    And most importantly, have fun with Wikiproofs!

    Best wishes,
    Alexander

  3. Jim Kingdon Says:

    I’m curious what you (slawekk) have in mind for item 2 (the readable presentation). Do you have such a thing for IsarMathLib? Part of why I ask is that I’ve tended to think there is a tradeoff between having a powerful prover and readability. The more powerful the prover, the harder it is for a human to see how the prover did its magic. Of course a prover can output a detailed set of steps, and we can certainly hope that it ends up being readable, but the one time I saw such a dump from coq it seemed pretty daunting (although no doubt that’s partly just an issue of whether someone has written a dumping tool which really aims for readability).

    On wikiproofs, I have largely fallen back to fairly extensive comments (roughly, if I had to write it down to enable me to write the proof, I put it on the wiki). I have relatively little way of knowing whether this a success or whether it just drowns everything in too many words (or both, for different readers). It of course would be more appealing if the formal proof language itself were more self-explanatory, but I have yet to see one which is (at least to my eyes).

  4. slawekk Says:

    Isabelle generated proof document for IsarMathLib is fairly close to what I have in mind. The FormalMath.org site is my attempt at improving this with better math notation, folding subproofs and hyperlinked theorem references. The drawback of Isar is that one can not see the proof steps above certain level of detail. In my opinion a two-layer approach with a high-level proof language on top of a Metamath-style language would be best. There is a post at Metablog that describes this idea very well.

    the harder it is for a human to see how the prover did its magic

    Being able to see the mechanics of what the prover did to fill the gaps in the high-level proof doesn’t have much to to with readability, at least how I understand it. The proof is readable when it is good at conveying knowledge of why the theorem is true. This means that it should look like proofs in standard (informal) math publications. This is the form people have been trained to absorb that information. For Coq the C-zar language is an example of making Coq verification scripts more readable.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: