Mathgate was a website for learning logic and mathematics through formal proofs.
It's essentially an archive now.

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.

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.

My feeling watching *The Imitation Game* was that Alan Turing was being (falsely) portrayed as a real-life Sheldon Cooper.
Charles Petzold wrote an interesting article
on this topic.

Proving Your First Theorems

(a video for theorem proving beginners)

Earlier

Proving Your First Theorems

(a video for theorem proving beginners)

December 10, 2014

October 3, 2014

September 27, 2014

September 20, 2014

September 13, 2014

September 6, 2014

August 30, 2014

August 23, 2014

August 16, 2014

Earlier