当证明可以被机器验证:OpenAI 722 篇数学论文背后的信任重构
一个不寻常的发布 昨天,OpenAI 发布了一批由内部前沿模型产出的数学新结果:722 篇论文,覆盖 500 个最重要开放数学问题中的 90 个,被外界称为"百年来数学界最重大的时刻之一"。发布流程参照普林斯顿高等研究院 AGMAI 委员会的公开建议,结果连同 Lean 形式化证明、10 份模型推理摘要一起放在 GitHub 仓库里,平均每条结果耗费约 3 小时 ChatGPT Pro 级算力。 很多讨论集中在"AI 解决了 90 个开放问题"这个数字上。但我认为,这次发布里最值得深挖的不是模型有多聪明,而是一个更结构性的事实:这批结果的信任基础,不是同行评议,而是 Lean。 理解了这一点,你就能看懂未来十年"AI 产出知识"的基本形态。 被绕过的同行评议 传统数学界确认一个新结果的流程是:作者写论文 → 投稿 → 审稿人逐行检查证明 → 发表 → 社区长期消化。这个过程平均以"年"为单位,且完全依赖审稿人的专业能力和耐心。历史上著名的教训不少:2012 年 Shinichi Mochizuki 声称证明 ABC 猜想,望月新一的 600 页证明至今没有被数学界主流消化或确认,双方僵持十余年没有结局。 现在设想一个 AI 一次性产出 722 篇论文。人类审稿力量根本不可能在合理时间内消化这个体量——这不是能力问题,是吞吐量差了几个数量级。如果沿用传统流程,这批结果会变成 722 个"望月新一式的悬案"。 OpenAI 的做法是把大量证明用 Lean 形式化。Lean 是一门编程语言,但它的类型系统允许把数学证明写成代码,由计算机内核检查。一个 Lean 证明一旦通过编译器检查,它的正确性就不依赖于任何人类的阅读和理解——你不需要信任作者,不需要信任审稿人,只需要信任一个可以独立复核的、几千行规模的验证内核。数学界对这类内核的信任,远比对任何机构或个人的信任更牢固。 换句话说,当产出者从人类变成 AI,“信任"必须从社会过程迁移到机械过程。Lean 不是这次发布的装饰品,它是整个发布能够成立的承重墙。 为什么是现在:形式化的成本曲线 形式化验证不是新想法。Coq/Rocq、Isabelle 这些证明助手已经存在了几十年,数学家陶哲轩从 2020 年代初就开始大力推广 Lean 和 mathlib,DeepMind 的 AlphaProof 也在 IMO 竞赛上拿过银牌级别的成绩。但形式化一直有个致命短板:把一个人类证明翻译成 Lean 的成本极高。形式化一个中等复杂度的定理,熟练工作者往往需要数周甚至数月。费马大定理这种级别的形式化,至今还是社区里流传的"多年计划”。 ...