数学界与 OpenAI 的争论，为什么让我想起了软件工程？

2026 年 10 月 6 日，OpenAI 在 GitHub 公开了一批由内部模型生成的数学研究稿件与声称的结果。围绕这些材料的争论，让我想起了 Coding Agent 刚进入软件开发时的讨论。

AI 会不会在推导中跳过关键步骤？生成的结果能不能相信？如果只有生成者自己知道它想表达什么，别人怎么检查和使用？这些问题，软件开发者并不陌生。

数学家的关切还有另一层。人类数学协会（AHM）在随后发表的声明中，强调数学研究应服务于人类理解。数学与人工智能咨询组此前的建议，也把帮助共同体理解和吸收结果，作为成果发布的重要责任。

作为软件开发者，我很认同其中一个问题：我们需要的究竟是更多产出，还是更多值得使用和继续研究的成果？

沿着 Coding Agent 的变化看下去，我觉得这场争论涉及三个相连的问题：机器怎样参与生产，正确性怎样得到保障，以及什么样的成果值得生产。

软件工程怎样开始接纳 Coding Agent

早期的 AI 代码经常编造 API、遗漏边界条件，或者写出能够运行却没有正确实现需求的程序。今天，开发者仍然需要处理这些问题。

与此同时，越来越多团队把 Agent 放进实际工作流程。规格说明让任务更明确，自动化测试和静态分析提供反馈，持续集成（CI）检查改动，代码评审（Code Review）帮助团队判断实现与设计。

这些安排使错误更容易被发现、约束和修正。模型能力的提高也在发挥作用，但可靠协作还需要把要求和反馈组织起来。

我认为，这比要求 Agent 复现某个程序员的思考过程更有用。不同的实现路径，可以依据同一组行为要求和工程标准接受检查。人类仍然需要理解关键设计，但判断一个结果是否可用，越来越依赖它能否接受独立验证。

因此，当 AI 生成的数学证明出现可靠性问题时，我首先想到的是：哪些要求可以写得更明确，哪些错误可以通过独立检查发现，哪些反馈可以用于下一次生成？

AI 会犯错，是设计验证体系的起点。具体错误暴露以后，也给了我们改进体系的对象。

数学已经有了更严格的验证工具

Lean 是一种编程语言，也是一种证明助手。使用它时，需要把数学对象、命题和证明写成计算机能够处理的形式，再由一个小型逻辑内核检查完整证明能否从声明的假设推出结论。

比如，要证明“任意自然数 n 都满足 n + 0 = n”，普通测试可以代入许多个数，检查这些例子是否成立；形式化证明则要依据定义或已有定理，给出适用于任意 n 的推导。Lean 检查的是这份推导。

证明可以由人写，也可以由 AI 生成。检查机制独立于生成者，也独立于另一个模型的评分。在所采用的逻辑、公理与检查器可信性的前提下，它能够为形式化命题提供普通软件测试所不能提供的保证。

还有一项工作，是核对形式化命题是否表达了原始问题。假设原问题讨论任意整数，形式化版本却只讨论正整数，那么证明即使通过检查，覆盖的范围也已经缩小。

这个错误可以成为具体的检查对象：对照原文与形式化声明中的取值范围，把零和负数纳入样例检查，核对新增的假设是否改变了问题。样例检查能够暴露一些错配，声明核对则直接考察证明对象。它们可以由工具辅助，也可以安排独立复核。

这对应软件工程里的两项工作：Verification，验证是否按规格完成；Validation，确认规格是否表达了实际目标。把对象、方法和检查结果分别记录，就能知道哪里出了问题，下一轮应该改进什么。

我看重的是这个方向：遇到可靠性问题后，继续寻找能够独立执行的检查与反馈。数学形式化提供了很强的基础，命题表达与语义对齐也值得继续发展工程方法。

Mathlib 的评审瓶颈是一个现实案例

Mathlib 是基于 Lean 的开源形式化数学库。Mathlib Initiative 的2026 年 10 月至 2027 年 3 月路线图报告，库已有超过 200 万行形式化数学内容、750 多名贡献者。

路线图将评审能力列为限制增长的主要约束：过去一年，评审吞吐量提高了，待处理的 PR 队列仍然增长。项目方计划维持每周约 130 次评审轮次的基础支持，扩大评审者队伍，并把重复意见转成自动检查，改善能够显示 Lean 声明变化的评审工具。

这是一组很熟悉的软件工程动作。生成、检查和知识集成有各自的处理能力，需要一起改进。

Formal Frontier 的项目说明解释了为什么通过证明检查后仍需评审：产物可能重复已有内容、采用不好的定义、忽略已有接口，或留下难以维护的证明。这些问题影响知识能否被复用。

2026 年 5 月的预印本 MathlibPR：形式化数学库的 PR 合并就绪评测也在研究这一层判断。论文摘要报告，其评测中的模型和 Agent 难以区分真正达到合并标准的 PR，以及通过构建、却仍需修订或从未合并的 PR。

Mathlib 已有的积压来自持续扩大的协作。路线图同时预期，未来下游项目会更多依赖 AI 生成。这让我看到，形式化社区已经在调整验证、评审与协作机制，以承接生产方式的变化。

通过验证之后，什么值得生产

即使检查和评审变得更高效，仍然需要回答：为什么要完成这项工作？

在 Coding Agent 的帮助下，很多实现的成本下降了。但不同的人和团队使用相近的工具，最后做出的软件仍然很不一样。

差别来自问题选择、需求理解、系统设计和取舍。一个团队可能更快地实现了大量功能，却始终没有解决用户真正需要解决的问题；另一个团队只做了几个关键改动，却明显改善了使用体验。

测试可以确认某项行为符合要求。至于这些要求是否值得投入、实现之后带来了什么价值，需要结合实际用途判断。

数学研究也有类似的问题。一项证明可以正确，一个结果也可以新，但它对知识的贡献还要看：是否揭示了新的结构，连接了原本分离的领域，提出了有价值的问题，或者让一批已有结论得到更清楚的解释。

数学家强调理解，至少有一部分是在关心这种继续研究的能力。别人读懂一个结果以后，能否把它用到新的问题上？一组证明能否逐渐组织成有解释力的理论？这些问题决定了知识如何继续增长。

我因此更倾向于把证明数量看作产出的一个指标，把形成理解、联系和后续研究的能力放进成果评价。当某类证明的生成成本下降，这些工作就更值得投入。

问题定义、抽象、验证和价值判断，也可以由 AI 参与。未来的分工可能继续变化，评价仍然需要落到成果究竟增加了什么。

重新看待这场争论

回到 OpenAI 的这次发布。其说明已经提到部分 Lean 形式化、修订与引用安排，以及支持后续理解的计划。接下来应该观察这些安排能否帮助研究者独立核验、理解和使用结果。

批量生成会增加共同体需要处理的材料，生成者应当承担相应的验证、整理与支持责任。这是新生产能力进入专业协作所需要的工作。

同时，我认为可以把成果质量要求与具体工作习惯分别考察。机器可以用不同于人类的方式探索，专业领域则需要发展能够检查这些探索结果、组织协作并积累知识的方法。

软件工程正在经历这样的变化。Agent 承担更多实现以后，规格、测试、评审和系统设计都需要跟着调整；团队还要判断哪些需求值得实现。数学形式化社区的实践，显示了类似的调整正在发生。

对于 AI 数学研究，我期待看到的进展包括：证明能接受更可靠的独立检查，命题表达更容易核对，评审中的重复问题得到自动处理，以及研究者能够从生成结果中发展出新的理解与联系。

这会把评价从生成了多少成果，推进到这些成果怎样成立、怎样被使用，以及怎样帮助知识继续增长。

当 AI 降低生产成本，专业工作的重点也会重新分配：保证结果正确，组织有效协作，并判断什么值得生产。

我认为，OpenAI 与数学界的争论值得继续讨论，正因为它把这三项工作同时摆到了我们面前。代码和证明的生成能力提高之后，软件与数学的价值仍然要在具体问题、设计和知识积累中形成。