Contact Person
J. J. Phillips
Bit Message:
Notice 1: Emails should not be considered private.
Notice 2: respects your anonymity. Your IP address is not recorded and this site uses no cookies. Enjoy your visit.
MathGateWelcome to Mathgate. Framework Foundation Schedule
Total Currently Available Unclaimed Treasures: 2.089 bitcoins
Total Unclaimed Treasures Remaining in the Treasure Hunt: 13.659 bitcoins

Note: Dr. Brown has announced that after the current treasure hunt has ended at the end of September 2014, he will sign (using PGP) certificates indicating who participated, using bitcoin addresses as pseudonyms. The idea is to provide pseudonymous academic credentials to the participants while not compromising their identity. More details can be found here.
Note: There is currently a proof with a corresponding 1 bitcoin treasure in Knaster-Tarski Fixed Points.

Bitcoin Theorem Proving Treasure Hunt Begins

Proving Your First Theorems
(a video for theorem proving beginners)
April 19, 2014
Knaster-Tarski Fixed Points (Proofs as Exercises) - paywall
Preamble Signature for Knaster-Tarski Fixed Points - free
April 12, 2014
Second-Order Propositional Logic - free
Binary Relations (Proofs as Exercises) - paywall
Preamble Signature for Binary Relations - free
April 5, 2014
Predicates and Extensionality (Proofs as Exercises) - paywall
Preamble Signature for Predicates and Extensionality - free
March 29, 2014
Introduction to the Zermelo-Fraenkel Set Operators I (Proofs as Exercises) - paywall
Preamble Signature for Introduction to the Zermelo-Fraenkel Set Operators I - free
March 26, 2014
Equality and Existential Quantification (Proofs as Exercises) - free
Preamble Signature for Equality and Existential Quantification - free
Second-Order Propositional Logic (Proofs as Exercises) - free

The bitcoin theorem proving treasure hunt is in progress.
On March 23, 2014, just over 14 bitcoins were buried underneath 557 formal proofs of mathematical theorems. The theorems are part of building the infrastructure of mathematics starting from a foundation of set theory in simple type theory. If you repeat the proof, you will get the private key for the part buried under that proof. Some of the proofs have only 1 mbit (0.001 BTC) buried under them. 28 of the proofs have 100 mbits (0.1 BTC) buried under them. Six of the proofs have a full bitcoin buried under them.
The proofs are divided among 25 documents, 2 of which were released March 26, 2014. The first document, Second-Order Propositional Logic, gave you the chance to find about 250 mbits worth of the hidden treasures before April 12. The second document, Equality and Existential Quantification, gave you the chance to find another 359 mbits worth of the hidden treasures before April 19. The remaining documents are being released according the schedule at the following link.
If you're interested in viewing the hidden treasures in the blockchain, they are the outputs of the following 25 transactions:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
Each transaction corresponds to one document and each output corresponds to a hidden treasure hidden under a proof in that document.
On March 30, 2014, I published the genesis block of the Mathgate promechard, available here. Information about how to verify the integrity of the data and that it was timestamped by the Bitcoin block chain on March 30, 2014, is available here. This, in particular, can be used to verify that the formal documents existed in their current form before March 30, 2014.