你有没有想过，那些教科书里被奉为圭臬的经典定理，可能从一开始就缺失了最关键的一环？哈佛商学院教授斯科特·科米纳斯（Scott Kominers）在经济学课堂里讲了数十遍的1976年奥曼定理，最近被一个AI系统揪出了根基上的漏洞——一个奥曼本人明确写下、却从未给出过证明的假设。

这一切源自Axiom Math公司构建的形式化验证系统。它不靠生成概率拼凑答案，而是用开源语言Lean把数学证明写成代码级精度：要么每一步逻辑编译通过，要么程序拒绝运行。当这套系统扫描奥曼的经典论文时，它毫不留情地标记出一个缺口——那个被经济学家们理所当然引用了近半个世纪的假设，在形式化框架下站不住脚。科米纳斯随后打给几位同行，得到的反应差不多是“这很合理，奥曼肯定知道”。但问题在于，知道不等于证明过。

打开网易新闻 查看精彩图片

更令人不安的是，信息经济学、平台设计、甚至联邦反垄断案的合并指南，都建立在以这个假设为起点的定理之上。一旦地基松动，一排看似稳固的理论大厦可能都需要重新审视。科米纳斯向《财富》杂志坦言，几乎所有仰赖这条定理的后续成果，都未曾有人从根基处做过形式化检验——直到现在。

这个发现是项目EconLib的首个公开成果。《财富》独家了解到，Axiom Math正试图用同样的方法重塑经济学理论在美国法律中的应用。这家位于洛杉矶的创业公司由CEO卡琳娜·洪（Carina Hong）创立，她曾是麻省理工和牛津训练的数学家，从斯坦福博士辍学创业，今年3月刚获得由门洛风险投资公司领投的2亿美元融资，估值达到16亿美元。

洪把公司的核心产品称作“经过验证的AI”。对她而言，唯一诚实的做法就是让数学和经济学的大门彻底对幻觉关闭。“要么从前提推到结论，要么别跑。”这或许代表了AI进入社会科学时，对严谨性最朴素的一次坚持。