一个被哈佛经济学课堂奉为必读、被全球经济学家引用了近五十年的定理，今年被一台AI系统挑出了一个漏洞，没有人注意到，直到一行代码拒绝编译。
这个定理是诺贝尔经济学奖得主罗伯特·奥曼在1976年提出的"一致同意定理"，也被称为"不能同意分歧定理"。它的核心论断简洁而优雅：如果两个理性的人拥有相同的先验信念，并且彼此的立场已成为共同知识，那么他们不可能仍然坚持相互矛盾的判断，也就是说，真正理性的人"不能同意分歧"。
这个结论深刻影响了信息经济学、平台设计、反垄断分析等诸多领域，是现代市场理论的一块基石。
然而它的证明从未被真正完成过，至少，没有人意识到这一点。
代码不会说谎，定理地基是空的
Scott Kominers 是哈佛商学院创业管理部门的 Sarofim-Rock 工商管理教授；哈佛大学经济系和哈佛大学数学科学与应用中心的教员；以及 a16z 加密货币研究合作伙伴。妮可·沃尔普
发现这个漏洞的，是一家名为Axiom Math的AI数学公司。今年早些时候，他们将奥曼的定理输入了Lean，一种开源的形式化证明编程语言。在Lean的逻辑体系中，每一个推导步骤必须像代码一样严格编译，差一步都无法通过。
系统标记出了一个问题：奥曼在构建定理时使用了一个假设，这个假设他自己提出过，但从未真正给出过形式化证明，而后来所有建立在这个定理之上的研究，都在无意间继承了这个未经证实的地基。
哈佛商学院教授、知名数学经济学家斯科特·科米纳斯是最早获知这一发现的人之一。他已经讲授这个定理数十次，在自己的研究中以它为基础，在哈佛的课程里将它列为必修内容。当Axiom Math的系统发出警报，他的第一反应是去询问同事。
"他们都说，'哦，这说得通，奥曼自己清楚这一点，'"科米纳斯告诉《财富》杂志。
问题是，奥曼从未真正证明过那些底层结构。
科米纳斯说，定理的证明"隐式依赖了比人们意识到的更多的东西"，而这些东西"从来没有被教过，也从来没有人注意到它们是相关的"。
这不是奥曼定理的崩塌，而是一次更令人不安的揭示：一个半个世纪以来被全球顶尖经济学家反复检验、引用和教授的证明，之所以没有人发现漏洞，是因为人类的同行评审系统依赖的是"足够多的聪明人觉得它说得通"，而不是每一步逻辑的形式化验证。
形式化验证：一场正在改变科学信任基础的革命
Axiom Math正是建立在这个判断之上。这家公司由MIT和牛津双料数学背景的卡里娜·洪（Carina Hong）创立，今年3月完成了2亿美元融资，估值达16亿美元。公司的核心产品是他们所说的"经过验证的AI"，也就是让AI不只是生成证明，还要用Lean语言把证明写出来，让机器强制检查每一步逻辑。
洪在Lean社区流传着一句话："每一个无法被形式化的证明，就是一个有问题的证明。"
在发现奥曼定理的漏洞之后，Axiom Math与科米纳斯共同启动了一个名为EconLib的项目，目标是为经济理论建立一个公开的、可机器验证的基础定理库，就像数学界已有的Mathlib那样，目前Mathlib已收录超过21万条经过形式化验证的数学定理。
这件事的影响远超学术圈。科米纳斯指出，大量反垄断案件的经济分析、市场合并审查的量化指标，都依赖于从未被形式化检验过的经济理论模型。"并购曾在这些定理的基础上获得批准，企业结构也因此被重塑，"他说。如果那些模型底下的假设本身就存在未经证实的前提，整个分析链条的可靠性就值得重新审视。
弗吉尼亚大学数论学家、Axiom Math顾问肯·大野（Ken Ono）对这场变革有更直白的表述。AI出现之前，数学或经济理论的权威性建立在人脑的积累和同行的认可上。AI出现之后，"知识变得廉价，但验证变得更昂贵，创造力的价值比以往任何时候都更高"。
五十年来，没有人发现奥曼定理的漏洞，不是因为这个领域的人不够聪明，而是因为没有人需要把每一步都逼到无法辩驳的程度，直到现在。
热门跟贴