TL;DR
This paper presents a blockchain-based system that facilitates collaborative formalization of mathematics and programs by combining human effort and AI tools, using smart contracts and incentive mechanisms to encourage participation.
Contribution
It introduces a novel blockchain platform integrating TCRs and smart contracts for collaborative formalization, automating proof synthesis and incentivizing contributors.
Findings
Demonstrated collaborative formalization of sorting algorithms' proofs
Showed how blockchain incentivizes and verifies contributions
Integrated AI tools with human efforts in proof development
Abstract
Formalization of mathematics is the process of digitizing mathematical knowledge, which allows for formal proof verification as well as efficient semantic searches. Given the large and ever-increasing gap between the set of formalized and unformalized mathematical knowledge, there is a clear need to encourage more computer scientists and mathematicians to solve and formalize mathematical problems together. With blockchain technology, we are able to decentralize this process, provide time-stamped verification of authorship and encourage collaboration through implementation of incentive mechanisms via smart contracts. Currently, the formalization of mathematics is done through the use of proof assistants, which can be used to verify programs and protocols as well. Furthermore, with the advancement in artificial intelligence (AI), particularly machine learning, we can apply automated AI…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
