数学界正在经历一场静默而深刻的焦虑。当 Science 杂志报道数学家们集体发出警告时，这个以严谨著称的领域正面临一个根本性问题：AI 生成的数学证明正在以难以验证的方式涌入学术体系，而传统的同行评审机制对此几乎束手无策。
这场焦虑的核心并非技术本身，而是验证权的转移。长期以来，数学证明的权威性建立在人类专家的逐行审查之上 —— 一位审稿人需要耗费数周甚至数月时间，跟随作者的思路穿越复杂的逻辑迷宫。然而，当 AI 能够在几分钟内生成看似严密的证明文本时，这种基于人类认知带宽的验证模式开始显露其局限性。
可验证性危机的实质
约翰霍普金斯大学数学家 Emily Riehl 指出了一个关键问题：大型语言模型生成的证明文本 "可能听起来正确、看起来正确、使用了正确的术语"，但 "其设计机制中没有任何东西能够保证它是正确的"。这是因为 LLM 基于概率生成响应，而非追求逻辑必然性。在数学领域，99% 的正确率意味着 100% 的不可信 —— 一个关键步骤的幻觉足以摧毁整个论证链条。
这种特性与数学的本质形成了尖锐冲突。帝国理工学院的 Kevin Buzzard 教授在 2017 年经历了一次 "数学中年危机"：他在审阅一篇论文时，经过与作者的长时间交流，仍然无法确定论证是否严谨。这促使他投身于 Lean 定理证明器的学习与推广，试图用机器验证替代人工审查的不确定性。
然而，形式验证本身也面临元层次的风险。Buzzard 警告说，即使 Lean 报告 AI 生成的代码是准确的，"它可能实际上并不代表数学家认为自己正在证明的那个定理"。验证工具只能检查形式正确性，无法判断形式化目标本身是否与数学家的意图一致。
人机协作的边界争议
Rutgers 大学的 Patrick Shafto 预测，五年内每位年轻数学家都将使用 AI。DARPA 在 2025 年初启动了名为 "指数级数学"(expMath) 的项目，旨在通过 AI 加速数学发现，将证明的细节构建工作卸载给机器。这种愿景描绘了一个数学家的角色从 "证明构造者" 转变为 "探索方向引导者" 的未来。
但南加州大学的 Aravind Asok 教授提出了根本性的质疑。他发现研究生们越来越多地使用 AI 生成作业答案，因此不再布置课后作业 ——"他们需要挣扎并以某种方式参与其中，才能真正建立自己的直觉"。Asok 的担忧触及了一个深层矛盾：如果学生通过 AI 绕过思维挣扎的过程，未来的数学家可能缺乏发现真正新前沿所需的创造力。
这种担忧超越了教学方法论，触及数学研究的本质。Asok 指出，错误在数学史上扮演了重要角色 —— 许多突破恰恰源于对先前错误的修正。如果 AI 驱动的证明追求 "一次性正确"，这种通过试错学习的机制可能被削弱。
形式验证的经济学转变
Martin Kleppmann 在 2025 年底的观察提供了一个工程化视角。他指出，传统形式验证的成本极其高昂：以 seL4 微内核为例，8700 行 C 代码的证明需要 20 人年和 20 万行 Isabelle 代码 —— 相当于每行实现代码需要 23 行证明和半个人日的工作量。
然而，LLM 正在改变这一经济算式。AI 不仅能够生成实现代码，还能在各种证明语言（Rocq、Isabelle、Lean、F*、Agda）中编写证明脚本。虽然仍需要专家指导，但完全自动化的路径已经清晰可见。Kleppmann 认为，当形式验证成本大幅下降时，"预期的 bug 成本低于验证成本" 的传统权衡将被打破。
更重要的是，AI 创造了一种对形式验证的需求。与其让人类审查 AI 生成的代码，不如让 AI 证明其生成的代码满足规约。证明检查器作为一小段经过验证的代码，能够拒绝任何无效证明，迫使 AI 代理重试 —— 这种机制天然抵消了 LLM 的概率性和不精确性。
可落地的人机协作参数
面对这场变革，数学界需要建立新的操作框架：
验证分层策略：将 AI 生成证明分为 "草稿验证" 和 "形式验证" 两个阶段。草稿阶段允许快速迭代，形式阶段使用 Lean 等工具进行机器检查。这种分层既保留了探索效率，又确保了最终输出的可靠性。
人机职责边界定义：明确划分机器与人类的分工 ——AI 负责 "填充细节" 和 "模式识别"，人类负责 "定义问题" 和 "验证意图"。正如 Kleppmann 所言，挑战将从 "编写证明" 转移到 "正确定义规约"。
学术伦理披露标准：建立 AI 辅助证明的披露规范，要求作者明确标注 AI 参与的程度和方式。这不仅关乎学术诚信，也为审稿人提供评估证明可靠性的必要上下文。
教育适应性调整：在研究生培养中重新平衡 "效率工具使用" 与 "基础能力训练" 的比重。Asok 的困境提示我们，完全禁止 AI 使用可能不现实，但完全依赖 AI 将削弱数学直觉的形成。
结论
数学界对 AI 渗透的警示，本质上是一场关于知识权威来源的辩论。当机器能够生成形式正确的证明时，人类数学家需要重新定义自己的价值 —— 不是作为计算的执行者，而是作为意义的诠释者和方向的把控者。
形式验证成本的下降为解决可重复性危机提供了技术路径，但它无法自动解决 "验证什么" 和 "为何验证" 的问题。人机协作的边界不是固定的技术参数，而是需要在实践中不断协商的社会契约。数学界正在书写的，不仅是一套新的验证标准，更是一种与智能机器共存的学术文化。
参考来源
- Science News: "Math long resisted a digital disruption. AI is poised to change that" (2026-04)
- Martin Kleppmann: "AI will make formal verification go mainstream" (2025-12)
内容声明：本文无广告投放、无付费植入。
如有事实性问题，欢迎发送勘误至 i@hotdrydog.com。