通过智能合约实现智能证明：基于去中心化市场的简洁且信息丰富的数学推导

现代数学建立在证明应可翻译为形式化证明的理念之上，形式化证明的有效性是一个客观问题，可由计算机判定。然而在实践中，证明是非形式化的，可能省略许多细节。一个智能体若相信某证明可展开为机器可验证的证明，便认为其有效。因此证明的有效性可能成为主观事项并引发难以解决的争论。故而，尽管有效证明的概念定义明确，确立有效性的过程本身却是一个复杂的多智能体问题。我们提出了SPRIG协议。SPRIG允许智能体以去中心化方式提出并验证简洁且信息丰富的证明；信任通过建立于智能体可在证明步骤中请求更多细节；若出现争论，必须隔离证明细节，若持续则下探至机器级细节，于此处自动解决。我们设置了赏金与押金的架构以激励智能体诚信行事。我们给出了SPRIG的博弈论讨论，展示了拥有各类信息的智能体如何交互，从而形成具有适当细节层次的证明树并证伪错误证明，并讨论了针对多种攻击的鲁棒性。随后我们分析了一个简化模型，刻画其均衡并计算智能体的信任水平。SPRIG被设计为在区块链平台上以智能合约运行。这使得匿名智能体可参与验证争论并贡献其信息。智能合约中介交互、解决争论，并保证赏金与押金按约定支付。SPRIG实现了新的应用，例如为开放问题发布赏金，以及创建衍生品市场，使智能体可注入更多与证明相关的信息。