Document Open Access Logo

Proofgold: Blockchain for Formal Methods

Authors Chad E. Brown, Cezary Kaliszyk , Thibault Gauthier , Josef Urban

PDF
Thumbnail PDF

File

OASIcs.FMBC.2022.4.pdf
  • Filesize: 0.63 MB
  • 15 pages

Document Identifiers

Author Details

Chad E. Brown
  • Czech Technical University in Prague, Czech Republic
Cezary Kaliszyk
  • Universität Innsbruck, Austria
Thibault Gauthier
  • Czech Technical University in Prague, Czech Republic
Josef Urban
  • Czech Technical University in Prague, Czech Republic

Funding

The results were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902, the ERC starting grant no. 714034 SMART, the Czech Technical University Global Postdoc Fellowship, the European Regional Development Fund under the Czech project AI&Reasoning no. CZ.02.1.01/0.0/0.0/15_003/0000466, and Amazon Research Awards.

Cite AsGet BibTex

Chad E. Brown, Cezary Kaliszyk, Thibault Gauthier, and Josef Urban. Proofgold: Blockchain for Formal Methods. In 4th International Workshop on Formal Methods for Blockchains (FMBC 2022). Open Access Series in Informatics (OASIcs), Volume 105, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/OASIcs.FMBC.2022.4

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Formal logic
  • Blockchain
  • Proofgold

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Chad E. Brown. Solving for set variables in higher-order theorem proving. In Andrei Voronkov, editor, Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings, volume 2392 of Lecture Notes in Computer Science, pages 408-422. Springer, 2002. Google Scholar
  2. Chad E. Brown, Mikoláš Janota, and Cezary Kaliszyk. Proofs for higher-order SMT and beyond. URL: http://cl-informatik.uibk.ac.at/cek/submitted/smt2022pfs.pdf.
  3. Chad E. Brown and Karol Pąk. A tale of two set theories. In Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44-60. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-23250-4_4.
  4. Alonzo Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5:56-68, 1940. Google Scholar
  5. John H. Conway. On numbers and games, Second Edition. A K Peters, 2001. Google Scholar
  6. Qeditas Developers. Qeditas technical documentation, 2016. URL: https://qeditas.org/docs/QeditasTechDoc.pdf.
  7. Warren E. Ferguson, Jesse Bingham, Levent Erkök, John R. Harrison, and Joe Leslie-Hurd. Digit serial methods with applications to division and square root. IEEE Trans. Computers, 67(3):449-456, 2018. URL: https://doi.org/10.1109/TC.2017.2759764.
  8. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Conference on Certified Programs and Proofs (CPP), pages 49-57. ACM, 2015. URL: http://doi.org/10.1145/2676724.2693173.
  9. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the kepler conjecture. CoRR, abs/1501.02155, 2015. URL: http://arxiv.org/abs/1501.02155.
  10. John Harrison. HOL light: A tutorial introduction. In Mandayam Srivas and Albert Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), volume 1166 of Lecture Notes in Computer Science, pages 265-269. Springer-Verlag, 1996. Google Scholar
  11. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. Google Scholar
  12. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, pages 56-68, 2003. Google Scholar
  13. Michael K. Kinyon, Robert Veroff, and Petr Vojtěchovský. Loops with abelian inner mapping groups: An application of automated deduction. In Maria Paola Bonacina and Mark E. Stickel, editors, Automated Reasoning and Mathematics - Essays in Memory of William W. McCune, volume 7788 of Lecture Notes in Computer Science, pages 151-164. Springer, 2013. Google Scholar
  14. Jin Xing Lim, Barnabé Monnot, Shaowei Lin, and Georgios Piliouras. A blockchain-based approach for collaborative formalization of mathematics and programs. In Yang Xiang, Ziyuan Wang, Honggang Wang, and Valtteri Niemi, editors, 2021 IEEE International Conference on Blockchain, Blockchain 2021, Melbourne, Australia, December 6-8, 2021, pages 321-326. IEEE, 2021. URL: https://doi.org/10.1109/Blockchain53845.2021.00051.
  15. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  16. F. Pfenning and C. Elliot. Higher-order abstract syntax. SIGPLAN Notices, 23(7):199-208, June 1988. Google Scholar
  17. Andrew Poelstra. On Stake and Consensus, 2015. URL: https://download.wpsoftware.net/bitcoin/pos.pdf.
  18. Dag Prawitz. Natural deduction: a proof-theoretical study. Dover, 2006. Google Scholar
  19. R. Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51:176-178, 1975. Google Scholar
  20. Bertrand Russell. The Principles of Mathematics. Cambridge University Press, 1903. Google Scholar
  21. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  22. M.H.B. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Rapport (Københavns universitet. Datalogisk institut). Datalogisk Institut, Københavns Universitet, 1998. Google Scholar
  23. Borching Su. Mathcoin: A blockchain proposal that helps verify mathematical theorems in public. IACR Cryptol. ePrint Arch., 2018:271, 2018. Google Scholar
  24. Petar Vukmirovic, Alexander Bentkamp, and Visa Nummelin. Efficient full higher-order unification. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 5:1-5:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  25. Bill White. Qeditas: A formal library as a bitcoin spin-off, 2016. URL: http://qeditas.org/docs/qeditas.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact