#### Description

{"ops":[{"insert":"Projects such as the "},{"attributes":{"link":"https://en.wikipedia.org/wiki/Millennium_Prize_Problems"},"insert":"Milennium Prize Problems"},{"insert":" exist to steer mathematicians to work on problems that are (or were at some point) deemed important by the wider community. Essentially, some people want certain mathematical statements proven, and are thus willing to pay money to whoever succeeds in proving them.Â \n\n\nBut how does the "},{"attributes":{"link":"https://en.wikipedia.org/wiki/Clay_Mathematics_Institute"},"insert":"Clay Mathematics Institute"},{"insert":" determine who was successful in proving a problem? How do we know that paper X is indeed a valid proof of statement Y? The answer is peer review. If enough reputable mathematicians claim that X indeed proves Y, the prize will be payed out.\n\n\nIn recent years however, more and more people are taking interest in a new way of doing maths - by using programming languages! Some time ago, some brilliant logicians have noticed that there exists a one-to-one "},{"attributes":{"link":"https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence"},"insert":"correspondence"},{"insert":" between mathematical statements and their proofs on one hand, and computer programs and their types on the other. What this means is that with a powerful enough computer language, one can define a statement one wants proven simply by defining a type in the language. The exercise of proving the statement then becomes one of constructing the value of the newly defined type. A big advantage of this approach is that we no longer need peer review to judge correctness of proofs! A computer algorithm can check if a given value (the proof) has the claimed type (the statement). If the type-checking algorithm returns true, we can be sure we have a proof of the statement on our hands!\n\n\nThere are many proof-languages out there today. The one we really like however, is "},{"attributes":{"link":"https://github.com/moonad/Formality"},"insert":"Formality"},{"insert":". It is fast, efficient, and it can run on the EVM.Â \n\n\nTaking all of this into account, an idea emerges. We could use Ethereum to create a trustless variant of the Milennium Prize Problems. A smart contract where anyone can contribute money towards a mathematical statement they want proven. Whoever is first to show a valid proof of a statement to the contract is paid the bounty on it. And the contract can judge the validity of the proofs itself.\n\n\nHowever, checking the type of any non-trivial value fully on-chain would quickly exceed the block gas limit. But there exists a way of doing computations that exceed the block gas limit on chain - we can use the "},{"attributes":{"link":"https://people.cs.uchicago.edu/~teutsch/papers/truebit.pdf"},"insert":"Truebit"},{"insert":" verification game to do that. We are already building "},{"attributes":{"link":"https://github.com/leapdao/EthereumMachineOracle"},"insert":"EMO"},{"insert":", a Truebit implementation with a generic machine backend.Â \n\n\nIn this grant we seek funding for developing the Formality type-checker backend for EMO. We want to open the world of mathematics to everyone, regardless of their background. Help us decentralise maths!\n"}]}