A Blockchain-Based Approach for Collaborative Formalization of Mathematics and Programs

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 reasoning tools in these proof assistants and (at least partially) automate the process of synthesizing proofs. In our paper, we demonstrate a blockchain-based system for collaborative formalization of mathematics and programs incorporating both human labour as well as automated AI tools. We explain how Token-Curated Registries (TCR) and smart contracts are used to ensure appropriate documents are recorded and encourage collaboration through implementation of incentive mechanisms respectively. Using an illustrative example, we show how formalized proofs of different sorting algorithms can be produced collaboratively in our proposed blockchain system.