MathGate
Framework Foundation Schedule
Treasure Hunt
Mathgate was a website for learning logic and mathematics through formal proofs. It's essentially an archive now.

While there are no ads on mathgate.info, I feel compelled to share this anti-ad coming from personal experience on October 9, 2014:
If you're choosing an airline, please do not choose AirBerlin. They cannot be trusted.
Of course, AirBerlin did not pay me to place this anti-ad, but I am doing it in response to losing hundreds of Euros to the lying bastards. So I suppose they anti-paid for the anti-ad.

The Egal proof checker used in the treasure hunt is now free and open source.

The treasure hunt ended Saturday, September 27, 2014. Thanks to everyone who took part.

Not counting the extra group theory problems, 8 people took part in the treasure hunt. Here are the list ranked by number of problems solved. Clicking on the address gives a PGP signed certificate (by my public key) indicating that the owner of the address participated.
1. 1MGb7YbEoHpBwvDtWpXZxxdnQvTrLXeZdd: 218 problems solved, approximately 2660 mbits claimed.
2. 1GQtYh4okefJKHf6hjj4wQY1638jdS8Mnp: 104 problems solved, approximately 859 mbits claimed.
3. 1Fv86iz25JBmaDKxC9VBXwHj3d8mhXoBuo: 30 problems solved, approximately 167 mbits claimed.
4. 17Ka6d26amrfnbHQAP5Fv2xmCjpG8H6WUy: 18 problems solved, approximately 1321 mbits claimed.
5. 19brLUpo6kV7erdvqjxdBK5KyXXqy6kL4i: 10 problems solved, approximately 52 mbits claimed.
6. 1695SHjDFwKpttZMU2HWb313g1echQkyEC: 8 problems solved, approximately 124 mbits claimed.
7. 1GdMi2Qt6zeLeniHoKxyVmXEMyLuG7aaF9: 2 problems solved, approximately 2 mbits claimed.
8. 1QDciDCbRAF2dRf1cwNvvgXvQq72Hg6eSL: 1 problem solved, approximately 10 mbits claimed.
Three other participants solved 4 of the "extra" 7 group theory problems:
  • 13eTCGuu6dH7fkSfQQDaq9AYAhhpQYrJ7v solved 2 of the group theory problems.
  • 12VTC6QB8Gd3tQy5oKr7FnvY7uK8jCZphq solved 1 of the group theory problems. I gave some (public) help in a reddit thread.
  • 16HvHkZvBxZTmENBFk1y7KDconKm3J2yQR "solved" 1 of the group theory problems by cut-and-paste. I had publicly posted the solution on the same reddit thread in an attempt to spark some interest in the treasure hunt.


  • Proving Your First Theorems
    (a video for theorem proving beginners)
    October 3, 2014
    A Formal Proof that Neil deGrasse Tyson is a Jackass.
    September 27, 2014
    Dependent Products and Simple Exponents of Sets
    September 20, 2014
    Functions as Sets
    September 13, 2014
    Dependent Sums and Simple Products of Sets
    September 6, 2014
    Ordered Pairs as Sets
    August 30, 2014
    Disjoint Unions
    Dependent Products and Simple Exponents of Sets (Proofs as Exercises)
    Preamble Signature for Dependent Products and Simple Exponents of Sets
    August 23, 2014
    Introduction to Ordinals
    Functions as Sets (Proofs as Exercises)
    Preamble Signature for Functions as Sets
    August 16, 2014
    Universes and Infinity
    Dependent Sums and Simple Products of Sets (Proofs as Exercises)
    Preamble Signature for Dependent Sums and Simple Products of Sets
    August 9, 2014
    Arithmetic on the Natural Numbers
    Ordered Pairs as Sets (Proofs as Exercises)

    Earlier