We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.GT

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Multiagent Systems

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

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.
Comments: This is an extended version of our accepted paper at The 4th IEEE International Conference on Blockchain (IEEE Blockchain-2021)
Subjects: Multiagent Systems (cs.MA); Computer Science and Game Theory (cs.GT); Logic in Computer Science (cs.LO)
Cite as: arXiv:2111.10824 [cs.MA]
  (or arXiv:2111.10824v1 [cs.MA] for this version)

Submission history

From: Jin Xing Lim [view email]
[v1] Sun, 21 Nov 2021 14:01:02 GMT (554kb,D)

Link back to: arXiv, form interface, contact.