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.
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!
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
If you're interested in viewing the hidden treasures in the blockchain,
they are the outputs of the following 25 transactions:
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
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.