过去几年 AI 在数学里的角色，从查资料做计算的助手，发展到能写长证明的推理模型，再到 2026 年开始出现研究级证明：不只给出自然语言证明，还同时附上专家检查、Lean 代码和可公开验证的证明文件。AI 数学研究正从"生成答案"走向"生成 + 验证"。这篇文章梳理这条线上的关键问题：规模化之后谁来验证、Lean 为什么突然重要、以及这对科研意味着什么。

一、真正值得关注的不是做对一道题，而是并行

模型偶尔解决一个数学问题并不令人不安，改变科研节奏的是并行能力。人的时间有限，一天能认真思考的问题有限；AI 系统可以同时尝试几十条证明路线、调用不同工具、让多个智能体分工（文献检索、推理、编程实验、证明尝试、结果检查），最后由主智能体汇总。已经有研究把几千个开放问题分别交给 AI 尝试，产出几百个候选结果。

问题随之而来：如果 AI 一天能生成过去几年才能产生的候选证明，人类没有能力一篇篇读完。

二、新瓶颈：从"找证明"变成"消化证明"

传统数学流程里最难的是找到一个可信的证明，动辄数年。如果生成速度不断提高，流程会变成：人类选题 → AI 生成候选证明 → 形式化系统验证 → 人类理解与重写 → 专家评审 → 知识整合。最慢的环节从"生成"移到了"验证、理解并整合"。

AI 可以快速增加论文、定理、猜想和机器证明文件，但专家注意力、阅读时间、理解能力和"什么真正重要"的共同判断没法同步增长。数学不是收集正确命题的数据库，一个结果要经过验证 → 理解 → 解释 → 比较 → 应用 → 整合才能成为共同知识。产出的增长速度可以远快于理解形成的速度，这可能是 AI 时代数学研究真正的矛盾。

三、"AI 会不会取代数学家"问错了问题

更有意义的问题是：当证明这种曾经昂贵的劳动变便宜后，人的价值往哪里移动？答案大概率是：选择值得研究的问题、判断结果是否重要、理解证明的核心思想、解释复杂结果、把分散结论连成理论、建设可长期复用的知识基础设施。所以更可能是数学研究内部的价值重新排序，而不是数学家消失。

数学共同体已经开始建立规则。AMS、SIAM、IMU 等的讨论方向基本一致：AI 可以参与，但过程透明、结果必须检查、责任由人承担。数学家内部态度分为几类——抵制自动化、坚持人的理解优先、规范使用（披露 + 核验 + 可审计记录）、以及主动参与设计 AI 的使用方式。第三种目前最容易落地。

四、Lean 为什么突然重要

AI 很会生成但生成的不一定可靠，所以需要一种只负责严格检查的工具。Lean 4 是编程语言，也是证明助理：把定义、假设、定理、证明全部写成形式化语言，交给 Kernel 检查，符合逻辑规则才接受。

举个最小的例子。数学论文里写"若 ff 和 gg 都是单调映射，则 g∘fg\circ f 单调"，人类三行推完就"显然"。Lean 不接受"显然"——你需要明确给出类型、序结构、映射定义、单调性假设、任取的 x,yx,y，以及每一步调用的是哪个前提，它才放行。这就是形式化证明的核心：把依赖人类默契的数学变成计算机能逐步核验的精确对象。

但 Lean 不会自己读论文：它擅长验证，不擅长把几十页 PDF 里的定义、"显然"的引理、领域默认知识翻译成形式化语言，人工形式化成本极高。于是 LLM + Lean 成了自然组合：LLM 快速生成（翻译命题、写证明代码、根据编译报错修改），Lean 严格验证，人类守护数学含义。这相当于写代码时"运行测试"而不是听 AI 说"应该能跑"。

五、一条工程化的验证闭环：VeriLoop

把上面的思路工程化，VeriLoop 的做法是把"整篇论文丢给模型"拆成受控流程：

  1. 读取论文：从 TeX 识别定义、命题、引理、定理、证明，组织成节点；
  2. 建依赖图：定理 B 依赖引理 A，先理清顺序，避免基础没完成就开始生成后面的证明；
  3. 搭 Lean 骨架：先固定定义、类型、定理声明和文件依赖，再填证明；
  4. 锁定命题：最大的风险不是 Lean 证明错，而是 AI 把原命题翻译错——先核对 Lean 命题和论文原文是否表达同一个数学主张，再锁定；
  5. 证明循环：LLM 生成 → Lean 检查 → 失败则根据报错修改 → 循环；最终证不出来的明确标记"未证明"；
  6. 最终审计：项目能否完整构建、有没有额外引入公理、哪些命题还有证明债务。

形式化不能取代同行评审：Lean 能判断"在这些假设下证明是否正确"，但判断不了问题重不重要、有没有创新、是不是几十年前已经证过。它的作用是替评审过滤机械性的逻辑错误，让专家把注意力放在思想和意义上。

六、形式化教材比形式化单篇论文更重要

VeriLoop 团队选择的落地项目是 Abramsky 与 Jung 的经典教材 Domain Theory，目标是建成别人能长期使用的形式化库：每个定理可追溯到原文、每个证明明确标记状态（已证明 / 受阻 / 待人工评审）、定义和 API 稳定可复用、开放协作。

这里有个关键洞察：单篇论文只讲自己的主线，到处是"由经典结果可知""显然"。Lean 不知道什么叫"经典"——底层理论没准备好，每形式化一篇论文都要重新补基础。所以更合理的路径是先把经典教材形式化成公共数学库，后续论文不断复用，就像编程不会每个程序都重写一遍字符串和网络协议。

这也预示了科研产出的形态变化：未来的论文可能不只是 PDF + 数据 + 代码，还包括形式化证明和自动验证报告——可执行、可检查、可复用。

七、对科研人的实际启示

  • 可验证科研（Verifiable Research）：生成越来越便宜，瓶颈全面转向验证。代码要编译测试 review，数学要 Lean 和专家检查，实验要数据和复现。以后问的不只是"AI 给了什么答案"，还有"我有什么证据相信它"。
  • 越来越值钱的能力：提出好问题、判断重要性、验证结果、解释证明、连接知识、建设基础设施（形式化库、数据集、审计）。
  • 数学教育：恰恰不是"AI 会了就不用学证明"。越能快速产生答案，越需要会判断答案对不对——独立推理、口头解释、识别隐藏假设、检查机器输出。
  • 评价体系：当"最先证出"不等于"贡献最大"，只看论文数量的评价会越来越失真。

如果只记一句话：**当生成答案越来越便宜，验证和理解就会越来越贵。**它同样适用于代码、论文、实验和数据分析。