Mathgate declares its purpose as a “website for learning logic and mathematics through formal proofs”. The author and owner of Mathgate is Chad E. Brown, who is also the author of Satallax – an automated theorem prover which has won a a couple of times on the CADE ATP Systems Competition. Mathgate is powered by a different prover, however, which is described as follows:
The particular approach taken here has elements in common with Automath (in that we use a small core language including proof terms), Mizar (in that we use Tarski-Grothendieck set theory and are attempting to form a library of formalized mathematics), Isabelle (in that we use a form of simple type theory as a framework) and Coq (in that we largely use the syntax of Coq for types, terms and proofs).
This shows that at least an alternative goal of the site is to build a library of formalized mathematics. However, recent announcement reveals that Mathgate was also to be a gambling site of sorts, bringing revenue to the owner. The idea was that people would pay up-front for access to exercises in proving theorems. Then they would participate in a treasure hunt – if their proof is correct and corresponds in some way (I guess by comparing the proof term) to the proof the author had in mind, they would be awarded some bitcoins. That idea did not fly, as the author says
I will no longer advertise it because I have no more hope of making it into a self-sustaining business. Since I’ll have to find another way to support myself, mathgate.info will only be a hobby and won’t be as active as it could’ve otherwise been.
Apparently the number of COQ programmers interested in formalized mathematics and gambling is too small.
I have to say I got encouraged by the treasure hunt and spent some effort to learn the proof language used on Mathgate. That was a rather frustrating experience for many reasons. The relevant information is scattered all over the site. There are instructional videos, and they are good, but there there is no tutorial that would describe tactics with examples of their usage. There is a document with a one-sentence description of each tactic, but with no examples and I think it simply does not tell everything needed. The error messages from the prover are rather unhelpful (like “Failure: Not a tp”).
Freek Wiedijk once gave a nice description of declarative vs. procedural proof languages
A declarative system is one in which one writes a proof in the normal way, although in a highly stylized language and with very small steps. (…) In a procedural system one does not write proofs at all. Instead one holds a dialogue with the computer. In that dialogue the computer presents the user with proof obligations or goals, and the user then executes tactics, which reduce a goal to zero or more new, and hopefully simpler, subgoals.
The Mathgate proof language is of the procedural kind – the user provides a series of tactics that manipulate the proof state and are intended to construct the proof term. However this is a procedural system with a twist – you don’t get any interaction. The tactics apply to the current goals, but you don’t get to see them. You need to have a very good idea on what each tactics does to the proof state to play the verification script (as I prefer to call the “proofs” in procedural style) in your head, but that intuition is difficult to bootstrap without seeing what happens when you apply a tactic.
As a result I kept getting stuck on trivialities. Typically in such cases one asks a question on some community forum, but there is no such thing for Mathgate. I really don’t remember having such hard time when I was learning the Isar proof language. Since the tactics supported by the Mathgate language are very similar to some COQ tactics I think the best way to learn the Mathgate proof language is to learn COQ first, and then use the experience.
After maybe 10 hours of watching videos, looking at provided example proofs and trial end error I finally was at the point when I was able to write some proofs that claimed to have milibitcoins associated with them. I did have some sense of accomplishment, even though I got “Your proof is correct but does not correspond to the declared treasure”.
I hope Dr. Chad E. Brown keeps working on Mathgate. The most important improvement would be to create a declarative language layer on top of the low – level tactics supported now – something like COQ’s C-zar. I am sure more people would be interested in formal proving if the experience was not so far removed from traditional mathematical practice.