Modern mathematics is built on the idea that proofs should be translatable into formal proofs, whose validity is an objective question, decidable by a computer. Yet, in practice, proofs are informal and may omit many details. An agent considers a proof valid if they trust that it could be expanded into a machine-verifiable proof. A proof's validity can thus become a subjective matter and lead to a debate, which may be difficult to settle. Hence, while the concept of valid proof is well-defined, the process to establish validity is itself a complex multi-agent problem. We introduce the SPRIG protocol. SPRIG allows agents to propose and verify succinct and informative proofs in a decentralized fashion; the trust is established by agents being able to request more details in the proof steps; debates, if they arise, must isolate details of proofs and, if they persist, go down to machine-level details, where they are automatically settled. A structure of bounties and stakes is set to incentivize agents to act in good faith. We propose a game-theoretic discussion of SPRIG, showing how agents with various types of information interact, leading to a proof tree with an appropriate level of detail and to the invalidation of wrong proofs, and we discuss resilience against various attacks. We then analyze a simplified model, characterize its equilibria and compute the agents' level of trust. SPRIG is designed to run as a smart contract on a blockchain platform. This allows anonymous agents to participate in the verification debate, and to contribute with their information. The smart contract mediates the interactions, settles debates, and guarantees that bounties and stakes are paid as specified. SPRIG enables new applications, such as the issuance of bounties for open problems, and the creation of derivatives markets, allowing agents to inject more information pertaining to proofs.
翻译：现代数学建基于一个理念,即证据应当被转换成正式证据,其有效性是一个客观的问题,可由计算机裁断。然而,在实践中,证据是非正式的,可能会遗漏许多细节。代理商认为如果相信证据可以扩展为机器核查的证据,证据就是合法的。因此,证据的有效性可以成为一个主观问题,导致辩论,这可能会难以解决。因此,虽然有效证据的概念是明确的,但确定有效性的过程本身就是一个复杂的多代理人问题。我们引入了SPRIG协议。SPRIG允许代理商以分散的方式提出和核实简明和内容性证据;委托人认为,如果他们相信证据可以扩展为机器核查的证明,那么,证据的有效性就会成为一个有效的证据。如果证据的有效性可以成为一个主观的问题,那么,那么,在机器一级,它可能很难解决。一个强势和赌注的结构,使智能代理商能够诚信地行事。我们建议对SPRIG的游戏理论性讨论,表明拥有各种精确的核查保证的代理商是如何在证据步骤中进行互动的;如果辩论,那么,那么,Srevil deal deal deal deal delial lial lial lial lade,我们就可以对各种的代理商的代理商进行一个正常的代理商进行交易。
相关内容
微信扫码咨询专知VIP会员