OpenAI 放出 722 篇数学论文：AI 证明如何验证、怎么用
一批由 AI 生成的数学结果被公开，数量达数百篇，覆盖十几个分支，正等待人类数学家核对。文章梳理围绕「过程是否重要」「谁来验收」「人的思考是否被外包」的三种分歧，并给出一套可执行的验证流程、审读清单与使用 AI 做推导的稳妥做法。
一批由 AI 生成的数学结果被公开，数量在数百篇量级，被归入几百个经典难题家族，横跨数论、代数几何、理论计算机、统计力学等十几个分支，接下来要交给人类数学家逐篇核对。消息传开后，讨论迅速分成两半：一半在惊叹「数学也被踏平了」，另一半在问——谁来看？看完算谁的？看懂了又说明什么？
对开发者来说，这件事真正的看点不是那个数字，而是它暴露出的新工作流问题：当模型能批量产出「看起来正确」的推导时，成本瓶颈从「生成」转移到了「验证」。这和代码生成已经发生过的故事几乎一模一样。
争论的三条主线
结果和过程，哪个才是收获
一种类比被反复提起：人手工把圆周率算到几百位已是极限，计算机能轻松算到几百万位，但这不说明计算机比数学家强，真正有价值的是人想出来的那个公式。放到数学证明上，结论是：解题过程中涌现的思路和方法才是核心资产，绕过苦思冥想直接拿到答案，收获有限。
反方不这么看：只要方法可复用、能继续拿去攻克别的问题，过程由谁完成并不重要；而且读懂 AI 的解法本身也可能带来启发，就像读一篇写法陌生的论文。
两种说法各有适用场景。涉及教学、人才培养和学科直觉的积累，过程不可替代，跳步会让人失去判断力；涉及工程实现和探索性研究，可复用的方法链条与最终正确性更值得优先保证。真正需要警惕的是把两者混为一谈：用「结果对了」去论证「能力提升了」。
谁来验收，验收完归谁
有人把这批论文形容成几百个待合并的 PR，指望着数学家来做 code review——这个比喻相当贴切，也点出了尴尬之处：产出方拿走了声量，审稿方付出了最贵的时间。
还有一层更微妙的情绪：学界对大张旗鼓的宣传姿态本来就警惕，尤其是当「谁定义问题、谁评估结果」这件事被商业叙事接管之后。类似的发布节奏在别的实验室也出现过，热度起落之间，真正沉下来做验证的仍然是那批人。
一个务实的共识是：验证必须有人做，而且必须能追溯到具体步骤，而不是一段语气自信的自然语言叙述。「模型说它证完了」和「证明可以被独立检查」之间隔着很远的距离。
人的思考会不会被外包
最尖锐的担忧不是失业，而是「提问的资格」也可能交出去——如果连问题都由机器提、答案由机器判，人还剩下什么位置。也有人觉得这属于多虑：人的生物学意义本来就不是创造价值，能享受服务没什么不好。
折中的底线大概是这样：提问权与验收权必须留在人手里，中间的计算与推导可以外包。 这条线守住了，工具越强越好；守不住，连判断「它错了」的能力都会慢慢丧失。
拿到这类结果后，怎么验证
如果你打算跟进其中某个结论，别急着读叙述性文字，先按下面的顺序过一遍。
第一步：形式化优先
能被形式化表达的命题，优先交给证明助手检查，人工只负责确认「形式化的陈述是否忠实于原命题」。这一步能挡掉绝大部分看似流畅实则断裂的推导。
# 以 Lean 为例，单文件检查
lake env lean MyProof.lean
# 项目级构建，看是否有未闭合的 sorry
lake build 2>&1 | grep -i sorry
形式化工具对版本敏感，依赖与工具链的版本务必锁定并记录，否则半年后没人能复现。
第二步：人工审读清单
形式化覆盖不到的（例如建模动机、结论解释、跨领域引用的合理性），用清单逐项核对：
| 检查项 | 关注点 |
|---|---|
| 命题陈述 | 与原始猜想是否一致，量词顺序、边界条件、退化情形有无被悄悄改动 |
| 外部引理 | 每个被引用的结论是否可查、是否被正确套用 |
| 关键跳跃 | 有没有用「显然」「易得」掩盖的核心步骤 |
| 反例测试 | 小规模枚举或随机测试能否证伪 |
| 计算部分 | 数值验证脚本能否被第三方独立跑通 |
| 结论强度 | 证的是特例还是通例，附加假设是否被淡化 |
第三步：记录与复现
把提示词、模型输出、人工修改、验证命令、失败尝试一并存档。失败记录尤其重要——它告诉你这个结论在哪种表述下会崩，比成功记录更有信息量。
用 AI 做推导时的稳妥做法
- 要求中间命题化。 让模型把证明拆成若干可独立检查的小命题，逐条验证，而不是一次性给出一篇完整论述。
- 禁止结论传递。 未验证的引理不能当作下一步的前提，否则错误会被层层放大。
- 交叉质询。 换一种表述或换一个模型重问同一个问题，看结论是否稳定；答案随措辞漂移通常意味着不可靠。
- 警惕过度顺畅。 数学推导里正常会出现卡壳与分支讨论，一路顺滑到底往往是最危险的信号。
- 给验证留出算力与时间。 批量检查、长时间迭代的会话对本地机器和网络稳定性要求不低；如果只是偶发跑一次，本地凑合即可，若需要持续数小时甚至跨天挂着跑，把工作负载放到一台长期在线的远程 Mac 上（例如整台机器托管在新加坡机房的独享方案）可以减少断线重跑带来的重复成本。
- 明确责任边界。 对外发布时写清哪些环节由模型完成、哪些由人验证，别用「AI 证明了」一句话糊过去。
几个容易踩的坑
- 被标题带走。 「震惊」「大地震」这类措辞会让人跳过验证直接转发。看到夸张表述，先找原始材料。
- 混淆不同分支的验证标准。 数论与统计力学的可检验性差别很大，一套流程套到底不合适。
- 把「不能形式化」当成「不能验证」。 无法形式化的领域仍然可以通过反例搜索、极限情形检验、独立重推来把关。
- 忽视归属与规范。 AI 参与生成的研究成果如何署名、如何披露，各期刊与机构的要求仍在变化，投稿前请以目标期刊和所在机构的最新规定为准。
- 一次性消费。 只记住「某个猜想被解决了」，却没人保存验证过程，等于什么都没留下。
小结
这轮发布的真正意义，也许不在于解决了多少难题，而在于它把「验证」推到了台前。生成变便宜之后，可靠性的定价权回到了能做检查的一方手里。对个人来说，可行的策略是：把提问和验收牢牢握住，把中间的推导尽量外包，并为自己准备一套可复现的检查流程。工具会继续变强，能判断「它对不对」的人，永远比只会按生成键的人走得更远。
