In this project a Web 3.0 platform for formal proofs will be developed and the usefulness of the platform for practical proof formalization will be demonstrated. The platform will combine AI tools for formalization, and blockchain-based tokens to create a central hub for formal mathematics on the web. The proposed work will include the development of translations for different logics, connections to particular proof assistants, the development of a blockchain explorer supporting formal proofs, the creation of convenient user and batch interfaces, and the investigation of the safety and security of the protocols.
More information on the project can be found on the project website.