About Theorem Marketplace
This is a theorem marketplace. You can place a bounty on a theorem, and if someone presents a proof of your theorem, your bounty will be paid to them. This is handled by a smart contract on the Ethereum blockchain in a (sorta) trustless way - so the bounty claimer doesn't need to worry about being paid. (The code of the contract is published here, and here is the contract's address in the blockchain.)
Note that you still need to trust the oracle that verifies the validity of proofs.
Theorems are written in Lean - a programming language and a theorem prover. Lean's awesome community developed this cool library called Mathlib. You can use it in your bounties and proofs - just type "import Mathlib".
The site currently runs on play money - the so called Sepolia test net. I plan to move to mainnet when the site looks secure. Currently, to play around with bounties, you need to get some Sepolia Ether (play money). Reach out to me and I'll wire you some.
You are most welcome to try and find any vulnerabilities in this site's work. Try to prove a false theorem, or claim a bounty without an actual proof, and it will be most helpful for securing the site against such attacks in the future.
The site is not a financial platform - no money is handled here, everything happens on the blockchain independently from the website. It's more like a classifieds site - theorems meet bounties, and the payments happen elsewhere.
I use SafeVerify for checking a theorem proof's validity. Kudos to GasStationManager who authored it!
This website is made by Vadim Fomin. My reason for creating this is a more general line of thought about how to accelerate scientific progress and make the societal aggregation of knowledge more efficient; seeking of mathematical knowledge seems more given to automating and incentivizing.
Check out my old post where this idea is proposed. Also, feel free to check out my other post with musings on the probabilistic nature of language.