Smart Proofs via Smart Contracts: Succinct and Informative Mathematical\n Derivations via Decentralized Markets

Abstract

Modern mathematics is built on the idea that proofs should be translatable\ninto formal proofs, whose validity is an objective question, decidable by a\ncomputer. Yet, in practice, proofs are informal and may omit many details. An\nagent considers a proof valid if they trust that it could be expanded into a\nmachine-verifiable proof. A proof's validity can thus become a subjective\nmatter and lead to a debate, which may be difficult to settle. Hence, while the\nconcept of valid proof is well-defined, the process to establish validity is\nitself a complex multi-agent problem.\n We introduce the SPRIG protocol. SPRIG allows agents to propose and verify\nsuccinct and informative proofs in a decentralized fashion; the trust is\nestablished by agents being able to request more details in the proof steps;\ndebates, if they arise, must isolate details of proofs and, if they persist, go\ndown to machine-level details, where they are automatically settled. A\nstructure of bounties and stakes is set to incentivize agents to act in good\nfaith.\n We propose a game-theoretic discussion of SPRIG, showing how agents with\nvarious types of information interact, leading to a proof tree with an\nappropriate level of detail and to the invalidation of wrong proofs, and we\ndiscuss resilience against various attacks. We then analyze a simplified model,\ncharacterize its equilibria and compute the agents' level of trust.\n SPRIG is designed to run as a smart contract on a blockchain platform. This\nallows anonymous agents to participate in the verification debate, and to\ncontribute with their information. The smart contract mediates the\ninteractions, settles debates, and guarantees that bounties and stakes are paid\nas specified.\n SPRIG enables new applications, such as the issuance of bounties for open\nproblems, and the creation of derivatives markets, allowing agents to inject\nmore information pertaining to proofs.\n