Impressum
Contact Person
J. J. Phillips
Bit Message:
BM-2cVzrek9Htn9Ki8rTGPREKTYmHuzD6Kzj2
Email:
jjphillips@bitmessage.ch
Notice 1: Emails should not be considered private.
Notice 2: mathgate.info respects your anonymity. Your IP address is not recorded and this site uses no cookies. Enjoy your visit.
MathGateWelcome to Mathgate. Framework Foundation Schedule

Bitcoin Theorem Proving Treasure Hunt Begins

Proving Your First Theorems
(a video for theorem proving beginners)
Congratulations to 1MGb7YbEoHpBwvDtWpXZxxdnQvTrLXeZdd who has found 173 mbits (so far) by proving theorems! There are still a lot of mbits out there, but someone is clearly in the lead. And stay tuned: on Saturday, April 19, a document will be released which has a treasure worth 1 bitcoin. It will be a proof of a form of the Knaster-Tarski Fixed Point Theorem. Good luck to everyone!
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 Foundation: Church's Simple Type Theory with Tarski-Grothendieck Set Theory - free
The bitcoin theorem proving treasure hunt has begun.
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, gives you the chance to find another 359 mbits worth of the hidden treasures before April 19. The remaining documents will be 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.