Proofgold: Blockchain for Formal Methods
Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, Josef Urban4th International Workshop on Formal Methods for Blockchains, FMBC 2022, pp. 4:1-4:15, 2022.
Abstract
Proofgold is a peer to peer cryptocurrency making use of formal logic. Users can publish theories and then develop a theory by publishing documents with definitions, conjectures and proofs. The blockchain records the theories and their state of development (e.g., which theorems have been proven and when). Two of the main theories are a form of classical set theory (for formalizing mathematics) and an intuitionistic theory of higher-order abstract syntax (for reasoning about syntax with binders). We have also significantly modified the open source Proofgold Core client software to create a faster, more stable and more efficient client, Proofgold Lava. Two important changes are the cryptography code and the database code, and we discuss these improvements. We also discuss how the Proofgold network can be used to support large formalization efforts.
BibTeX
@inproceedings{cbcktgju-fmbc22,
author = {Chad E. Brown and Cezary Kaliszyk and Thibault Gauthier and Josef Urban},
booktitle = {4th International Workshop on Formal Methods for Blockchains, FMBC 2022},
doi = {10.4230/OASIcs.FMBC.2022.4},
editor = {Zaynah Dargaye and Clara Schneidewind},
pages = {4:1--4:15},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
series = {OASIcs},
title = {Proofgold: Blockchain for Formal Methods},
url = {https://doi.org/10.4230/OASIcs.FMBC.2022.4},
volume = {105},
year = {2022}
}