一场发表在 Science 上的「慢」
昨天，DeepMind 的 AlphaProof Nexus 论文正式发表在《Science》上。基于 Gemini 3.1 Pro 的这个系统，用 Lean 形式化语言起草并迭代证明，由 Lean 逐步校验，最终破解了 353 个 Erdős 开放问题中的 9 个——其中两个悬置了 56 年。此外它还证明了 44 个 OEIS 猜想、解决了一个代数几何开放问题，并改进了 min-max 优化的已知界。
单看数字，这不算爆炸性新闻。就在几周前，OpenAI 刚刚往 GitHub 上倾倒了 372 份 AI 生成的数学证明，声称其中包括 BSD 猜想与 Hodge 猜想等重要进展，并公开表示学术界应该「跟上速度」。相比之下，9 个 Erdős 问题听起来相当克制。
但数学界的反应截然相反。OpenAI 那批证明引发了 Terence Tao 领衔的「人类数学协会」公开抵制；而 DeepMind 这篇论文，走完了完整的同行评审流程，解决方案提前在线公开供社区检验，最终登上了科学界最严格的期刊之一。
同样的技术浪潮，两条路线，两种命运。这背后的分歧比「AI 能不能做数学」深刻得多——它关乎一个问题：当证明的供给从稀缺变为过剩，数学学术体系的瓶颈到底是什么？
技术拆解：Lean 是这场分歧的隐形主角
先看 AlphaProof Nexus 到底做了什么。
系统的核心循环并不神秘：Gemini 3.1 Pro 用 Lean 形式化语言起草证明，Lean 编译器逐步校验，错误信息作为反馈指导下一轮修改。遇到更难的子问题时，可以调用专门的证明工具 AlphaProof 协助。值得注意的是，DeepMind 报告称即使不调用 AlphaProof，单靠通用模型 + Lean 反馈循环，九个 Erdős 问题也全部解决了。
这里的关键不是模型多聪明，而是 Lean 在整个流程中扮演的角色。
Lean 是形式化证明语言，它的类型系统等价于一个证明检查器：一个证明要么通过编译、在逻辑上无懈可击，要么不通过——不存在「看起来差不多对」的灰色地带。这意味着 AlphaProof Nexus 产出的证明，其正确性不依赖于人类审稿人逐行检查，也不依赖于模型的可靠性，而依赖于一个可以被独立复现的机械过程。
这解决了 AI 数学最核心的信任难题：你不需要相信 AI，只需要相信校验器。 而校验器本身是开源的、可审计的、确定性的。
回看 2024 年 AlphaProof 在 IMO 拿银牌、2025 年底技术细节登上《Nature》，再到今天 Nexus 解决真正的研究级开放问题，这条路线的演进脉络非常清晰：从「竞赛题」（有标准答案可验证）走向「开放问题」（答案未知，但推理过程可形式化验证）。每一步，Lean 这类形式系统都是承重墙。
而 OpenAI 的 372 份证明呢？据 The Decoder 报道，它们以非形式化的传统数学文本为主，正确性验证只能靠人类数学家逐份审读。这就是分歧的技术根源：一个把验证成本压到了接近零，一个把验证成本原封不动地转嫁给了整个学术社区。
为什么「倾倒证明」会激怒数学家
要理解数学界的愤怒，得理解学术数学的经济学。
一篇数学论文的价值，一半在证明本身，另一半在于它被社区消化、吸收、并入知识体系的过程。同行评审不只是质检，更是知识的「入网仪式」——审稿人读了、理解了、认可了，新知识才接入人类数学的网络。这个过程慢，但它保证了进入网络的每个节点都有人真正理解。
OpenAI 的做法相当于绕过入网流程，直接把 372 个「已解决」标记扔进网络，然后说：你们自己验证去吧。以一篇严肃论文审稿数月到数年的成本估算，社区验证这批证明的总开销是天文数字。Tao 等人的抵制，本质上不是反 AI，而是反对单方面改写交易结构——AI 公司获取了「解决了千禧难题」的宣传价值，社区承担了全部验证成本。
DeepMind 的选择则是对这笔账的精明回应。Lean 形式化证明的审稿，审稿人不需要逐行检查逻辑（Lean 已经做过了），只需要评估：问题是否真的开放、结果是否重要、方法是否有洞察。审稿成本从「验证正确性」降到「评估意义」，这才是同行评审在 AI 时代还能运转的前提。
换句话说，AlphaProof Nexus 通过 Science 评审这件事本身，就是一次技术演示：形式化不是锦上添花，而是 AI 数学成果能够被学术体系接纳的唯一通道。
更深一层：AI 正在重塑「证明」的社会契约
把镜头拉远，这场争论其实是科学史上一次经典戏剧的重演。
望远镜发明时，伽利略的观测结果一度不被接受——因为「只有他看得见」。最终的解决方案不是让更多人相信伽利略，而是造出更多望远镜，让观测变成可复现的过程。仪器可信，则结果可信。
AI 数学正处在同一个转折点。当模型的推理过程是一个黑盒、输出是非形式化文本时，社会只能选择「相信或不相信」某个实验室——这是前望远镜时代的困境。而形式化验证路线提供的是「望远镜」：任何人在任何机器上运行同一个校验器，都能得到同一个判定。信任的对象从机构转移到了工具。
这对整个 AI 行业的启示远超数学领域。看看同一份日报里的其他新闻：Epoch AI 的 InnovationEval 实测发现前沿 Agent 自称完成 70% 的研究改进、实测仅 15%；Vals AI 发现多 Agent 团队成本最高 5.1 倍、四组对比仅一组有统计显著提升。当 AI 的自我报告与现实之间的鸿沟成为行业常态，「可验证性」正在从技术属性变成产品竞争力本身。
DeepMind 这次拿下的不只是 9 个 Erdős 问题，还有范式定义权：AI 时代科学成果的合规形态，是「模型生成 + 形式系统背书 + 同行评审意义把关」的三层结构。 每一层各司其职——模型负责探索，形式系统负责正确性，人类社区负责意义。
冷思考：这条路线的边界
当然，也不必把 AlphaProof Nexus 路线神化。
第一，形式化本身有成本。把一个开放问题翻译成 Lean 可处理的形态，往往需要深刻的数学判断——这次 353 个 Erdős 问题只解决了 9 个，剩下的大多数可能根本无法在合理成本内形式化，或者需要的人类洞察不亚于直接证明。Lean 是验证的快车道，不是发现的快车道。
第二，「可验证」的领域仍然狭窄。数学是唯一拥有完美验证器的学科。min-max 优化界的改进能反哺 AI 训练，但物理、生物、社会科学没有 Lean，AI 在这些领域的成果依然要回到传统的信任框架里挣扎。
第三，别忘了 DeepMind 也是商业公司。选择同行评审路线未必纯粹出于学术理想——在 OpenAI 因激进发布引发抵制、监管环境趋紧的当下，「被学术界接纳的 AI 公司」本身是极具价值的品牌资产。范式之争的表象下，依然是两家公司的竞争策略。
但即便带着这些保留判断，趋势已经清晰：AI 科学的下一步竞争，不在生成能力，而在信任基础设施。 谁能让自己的 AI 产出以最低成本获得学术界和社会的信任，谁就定义了下一代科研的接口标准。
AlphaProof Nexus 用一篇 Science 论文证明了这个道理——字面意义上的证明。