上周的数学圈，出了两条几乎同时刷屏的新闻。第一条：OpenAI 在 GitHub 上一次性倾倒 700 多份数学手稿，声称自家未公开的模型解决了大量未解难题，数学家们的反应以震惊和反感为主，一个由菲尔兹奖得主牵头的组织公开呼吁抵制。第二条：Google DeepMind 的 AlphaProof Nexus 在顶级期刊《科学》（Science）上发表论文——独立解决了 353 个精选开放 Erdős 问题中的 9 个，其中两道已经悬置 56 年，全部证明经过完整的同行评审。
一个把结果泼进代码仓库，一个把证明交给审稿人。同样是 AI 做数学，路线之争已经摆上台面。
一、它到底解了什么
先看成绩单。根据 10 月 8 日发表于《科学》的论文，AlphaProof Nexus 的成绩单是：9 道 Erdős 开放问题、44 条 OEIS（整数序列在线百科）中的猜想、1 个代数几何领域的开放问题，还把 min-max 优化中的一个已知上界向前推进了一步。
Erdős 是二十世纪最高产的数学家，生前留下了上千个猜想。这些题目有个共同点：表述小学生都看得懂，但解起来可能耗尽几代数学家的心血。被解出的 9 道中，有 2 道整整悬置了 56 年。更值得注意的是成本——据报道，每道题的机器推理成本只要几百美元。
二、它是怎么解的
这不是「模型随口一说」，而是一套严格的工作流。系统以 Gemini 3.1 Pro 为核心：模型用形式化语言 Lean 起草证明，每写一步，Lean 就立刻机器验证这一步是否成立；报错信息再喂回给模型，引导它修改下一版。遇到更难的子问题，可以呼叫专门的证明工具 AlphaProof 来助攻。DeepMind 表示，即使没有 AlphaProof 帮忙，那 9 道 Erdős 问题也是 Gemini 独自解出的。
关键点在于：整个过程的每一步都可被机器独立验证。数学界最不缺的就是「听起来对」的证明，最缺的就是「保证没错」的证明——这套流程恰好补上了后者。
三、真正的看点：同行评审这四个字
如果只是「又解了几道题」，这篇论文不会这么出圈。它出圈，是因为时机。就在论文发表前两天，OpenAI 把 700 多份数学手稿一次性丢上 GitHub，声称解决数百个未解问题，没有经过任何审稿。数学家们的愤怒不难理解：每份手稿长达数十上百页，没有一篇经过独立验证，人类专家根本看不完。由陶哲轩等人牵头的 Association for Human Mathematics 随即呼吁数学家停止与 OpenAI 在这类项目上的合作。
数学界对这种事是有心理阴影的。2025 年 10 月，OpenAI 曾宣称模型自主解决了 10 道 Erdős 问题，很快被数据库维护者 Bloom 证伪——那 10 道「新解」其实是系统检索到了已有的旧论文，只是数据库没收录。
而 DeepMind 选择了最「老派」的方式：结果先公开，论文送审，最终登上《科学》。同行的评价很直接——数量上 OpenAI 碾压，但认证含金量完全反过来。
四、也要泼点冷水
- 9/353，约等于 2.5%。这是从精选出的 Erdős 问题里解出的比例，离「横扫」差得很远。
- 「低垂果实」。陶哲轩此前评价同类 AI 解题成果时说过，这些多属于低垂果实——方法成熟后，原本要耗专家几天的心力现在几分钟就能拿下，但攻坚的味道还谈不上。
- 验证 ≠ 重要性。机器验证保证的是「证明无误」，不保证「问题重要」。哪些题目值得 AI 去攻，仍然需要人类数学家的判断。
所以更准确的说法是：AI 把数学证明的「验证成本」打下来了，但「提出好问题」的能力，仍然稀缺。
五、对普通人的三点启示
- 看 AI 成果，先看它过了哪道验证关。机器可验证（Lean 形式化）、同行评审、专家背书，这三层的含金量天差地别。下次再看到「AI 解决了某某百年难题」的标题，先问一句：谁验过？
- 「数量轰炸」正在成为新的公关策略。700 份手稿的阵仗，换成任何人都会被淹没。面对这种发布方式，数学界的抵制本质上是在保卫一种共识：科学结论的效力来自验证，不来自音量。
- 人机分工的雏形已经清晰。AI 负责在海量候选路径里快速搜索和试错，人类负责提问题、判重要性、做最终把关。这套分工不只在数学成立——写代码、做研究、做决策，逻辑是一样的。
一百年前，数学证明的正确性靠大师的信誉担保；今天，一台机器可以一边写证明、一边自己验错，成本只要几百美元。
DeepMind 和 OpenAI 的分歧，其实不是技术之争，而是「科学该怎么被生产出来」之争：是把半成品成吨倒向社会，还是把每一个结论都钉在可验证的轨道上。
答案，数学界已经用投票给出了。
科技不高冷，AI很好用。
我是鱼叔，关注我，带你一起玩 AI！
参考：Google DeepMind《Advancing mathematics research with AI-driven formal proof search》（Science, 2026-10-08）· The Decoder · remio.ai · arXiv 相关综述与报道