Egal: A Mathematical Proof Checker That Doesn't Matter

Dr. Chad E. Brown

September 30 2014

Today I announce the free and open source release of the Egal proof checker. There are 1.175 bitcoins (update: 0.68 bitcoins) worth of treasure in one last document about Category Theory (CategoryProblems.mg). There is no deadline. I will never release the solutions. More details are below.

Download Egal

In the Summer of 2014 I used a proof checker I had written to support a Bitcoin theorem proving treasure hunt. The code worked, but I didn't want to release it until I had cleaned it up and done some refactoring. In the end, I decided to do minimal cleaning of the code and gave up on refactoring it, so the source code released in September 2014 is very close to what was actually used in the treasure hunt. The treasure hunt itself never gained much traction. The number of people interested in theorem proving is small, and the same is true of the number of people interested in cryptocurrency. Empirically, it seems that the intersection of these two niches has a single digit cardinality.

In spite of the failure of the treasure hunt, it wasn't a total loss. I gained some valuable experience writing bitcoin related code, producing explanitory videos and using the promechard private metablock chain idea. Hopefully some of this experience will be helpful as I take the next steps in my life. Also, I have written a foundation for mathematics into the sixth year of the block chain. That is eternal.

Given the minimal interest, I eventually decided to name the proof checker Egal. Egal is a German word that more-or-less means something that doesn't matter. It also has what could be a more positive interpretation: equality (égalité in French). The Egal proof checker does represent a kind of social equality that I do not see anywhere else in human affairs. Either a proof is correct or it isn't. The race, gender, religious views or political views of the prover do not matter. All that matters is correctness of the proof. Also, since all propositions have a global identifier, Egal contains the ability to check if a proposition has been proven before. If someone maintained an appropriate database, it would matter whether or not someone is the first to prove a theorem. When I imagined a world with Egal, I imagined a world in which correctness and originality matter but properties such as race, gender and so on do not.

There is also a hastily written manual explaining how to use Egal and gives some guidance as to the code. In principle someone could use it to set up their own treasure hunt, and hopefully the manual provides enough information for someone to do that. I can't give any advice regarding how to make it popular beyond this: I did something wrong, so don't do that.

I am also releasing the Coq code which verifies the algorithm for the parser Egal uses. This is documented in the manual.

A few other tangentially related pdfs are included with the source. One paper presents Zermelo's 1908 proof of the well-ordering theorem. A formal version of this proof was part of the treasure hunt. Another paper covers a nonstandard way to represent pairs and functions as sets and some of the nice properties these representations have. Formal versions of number of these results were included in the last few documents of the treasure hunt. Another paper describes a semantics for an intuitionistic higher-order logic supporting higher-order abstract syntax. This could be the starting point if someone wanted to modify Egal to support higher-order program verification instead of formalizing mathematics.

Finally, as mentioned above there are some final treasures. One of the formal documents included with the release, CategoryProblems.mg, has 35 unproven theorems with hidden treasures (for a total of just over 1 bitcoin). I have the 35 corresponding proofs, but I won't release them. I'll leave the treasures there until someone finds them with one caveat: Each time the bitcoin price increases by an order of magnitude I may collect the treasures and replace them with smaller treasures. For example, if the bitcoin price were to reach 3000 Euros, I would probably collect the treasures and replace them with treasures with the decimal moved by one (for a total of just over .1 bitcoin).

I plan to move on to other things but will leave the mathgate.info site up for the foreseeable future. I no longer have plans to add more content to the site. It's been a long time since I've read Ayn Rand's The Fountainhead. If I recall correctly, when no one would pay Roark to design buildings his way, he went to work breaking rocks in a quarry. Breaking rocks in a quarry doesn't sound bad at this point.


Update (May 21 2016): While most of these last treasures have been claimed, there are still six unclaimed worth a total of 0.68 bitcoins:
Update (June 7 2017): The bitcoin price is relatively close to 3000 EUR, so as I said above, I am likely to replace these last six treasures with one tenth of the bitcoin value. I felt morally compelled to preannounce this, so I wrote this reddit post:

It never seems to have shown up as "new" and was removed, so it looks like this

Well, I did what I could. It's a nice reminder three years later of why I gave up on all of this. Again, Egal!