来源： Invited Talk 02 · Remy Degenne 播客： ICML 2026 · AI4Research 分类： AI 研究 原文发表： 2026-07-10 纪要生成： 2026-07-13
从"AI 前就在用 Lean"的资深维护者视角，讨论能否用 AI 加速形式化数学：Lean 能给出比人工评分廉价得多的正确性检查，AI 已能把新证明"从 mathlib 出发"自动形式化；但当前 AI 生成的 Lean 代码冗长、重复、缺乏泛化、永不学习、且证明了正确定理却未必陈述了你想要的东西——真正缺的是"信任大规模 AI 代码库"的工具、更好的 harness、以及 AI 自己写自动化（tactics）的能力。
紧接 Gukov"如何用 AI 解更多数学问题"，Degenne 聚焦其中一环：如何检查这些 AI 产出的东西。他用 Lean（也存在 Rocq、Isabelle 等，但 Lean 是他本人及 AI for math 研究用得最多的）。
Lean 是什么：首先是一门功能完备的函数式编程语言，几乎任何程序都能写；对数学更重要的是它也是证明助手——可陈述定理、写证明，写完后 Lean kernel 会检查证明，无报错即代表你陈述的东西已被 Lean 验证通过。但 Lean 本身不是 AI，不会自动证任何东西，它是一个"你或你的 AI agent 在其中写证明、以供检查"的系统。两个层面可结合：既能给程序写证明（软件验证），也能写产生证明的程序——后者至关重要，因为高级理论不能永远只用最基础的构件手搓，需要把大段证明自动化。
在 Lean 里做数学长什么样：一个示例 Lean 文件（顶部还有一行没显示的 import 数学库）：先定义对象（measurable space、probability measure、stochastic process、filtration），然后给两个相似陈述——冒号是"假设"与"待证结论"的分隔符；这里证的是"一列子高斯随机变量之和超过 ε 的概率被某指数上界控制"。正确时证明只需一行（直接调用库里已有引理）；出错时（如他删掉某个假设、使某引理名失效）会看到红色波浪线，并能得到"哪里、出了什么错"的详细信息。
Lean 对 AI for math 的意义在于大幅降低检查成本。他引 DeepMind 关于 Aristotle 系统的报告：在一批 700 道英文数学题上运行（全程无 Lean，输入输出都是英文），系统产出 200 个候选证明；要检查它们，先经第一轮人工评分筛到 63 个正确，再进一步评估——因为"正确≠有意思"，一个证明可能因误解了题意而把问题变平凡后解掉，进一步筛到 13 个。问题是：当你自己做研究、想让 AI 帮你交流想法、证某定理时，你面对的是产出 200 个的那个系统，不是 63、更不是 13。希望是用 Lean 这样的形式系统取代最初那轮人工评分——它不能取代"最终判断你是否证了你想证的定理"，但能对证明正确性做一次快速检查。
Lean 的主数学库是 mathlib：开源、社区驱动，涵盖当今本科数学课程的大部分。关键区别是"它不是 arXiv"——不是随便放形式化的地方，更像一本书：力求一个对象只有一个定义，而非 20 个略有差异的平行定义。评审过程投入大量精力，使数学被泛化、放到正确位置、对可预见应用可复用。它几乎完全由人手写，近期虽有极少数经严格 curated 的 AI 贡献，但把 AI 代码并入 mathlib 很难。当前 mathlib 在增长、增长速度本身也在略微加快，但并未出现"有了能写 Lean 的 LLM 就该有的那种戏剧性加速"——正因为很难让 AI agent 产出那种通用、良好组织、高质量的库代码。
他给出的现状判断：如果你已有某东西的有效证明、想用 Lean 落实以求保险，那么让 AI agent 来做是完全合理的——订阅你偏好的 AI agent，在 VS Code 里让它对照你的 LaTeX 证明写一个 Lean 项目并检查，"这是可行的"。已有很多人形式化整本书/文章/长证明，三个例子：
他用一张"很不精确"的图：中心圆代表理想化的本科课程水平；从圆心沿某方向外扩即某个数学领域；中间实心蓝区是 mathlib——几乎在每个方向都接近本科水平，个别方向凸出到研究级。观察到的现象是：做自动形式化时，人们每次都从 mathlib 出发，去形式化它外围"晕轮（halo）"里的新结果；随模型能力提升，能形式化离 mathlib 越来越远的东西，晕轮越来越大。但从未看到：晕轮里那些新形式化并入实心蓝区、成为可继续往上盖的地基。每个新形式化都从 mathlib 重启。于是核心问题是：能否让 AI 加速这件事，让我们边想出证明、边把它形式化，从而更快抵达研究级数学？
Degenne 自述是"AI 前就做 Lean"的人：做了 5 年 mathlib 维护者，也领导多人协作的形式化项目（大家一起讨论、定计划、形式化更多数学，目标是并入 mathlib）。
这些项目里出现了新东西：AI 生成的 pull request（PR）。项目的一个目标是"或许能比 mathlib 走得更快一点"——因为 mathlib 的评审流程很慢、评审者被 PR 淹没。于是想吸纳 AI 生成的 PR，但它们巨大、质量可疑（很依赖所用模型、以及驱动模型者的经验）。
他点出一个关键痛点——AI 永远不学习：当你评审一个人类新手写的（很烂的）PR，你留很多意见、合并很慢，但这个人在学习，几个月后就能稳定产出高质量、你能秒合并的代码；而 AI agent 的 PR，你花两小时评审这一个，下一个还得再花两小时，它唯一"变好"的时刻是换了新版本模型。
本周他正在把自己与学生 Ridwan Yaguti、同事 Emilie Kaufmann（Inria）的最新统计论文（关于 response-adaptive targeting strategies，可用于临床试验，研究某些随机变量的渐近正态性等，用到 martingale 工具如大数定律、重对数律 LIL）做自动形式化。这些结果恰好就在 mathlib 之上一层：mathlib 没有 martingale 版大数定律，但从现有东西不难得到，论文其余部分所需的非 mathlib 前置也很少。纯从代码、无上层 harness。
进展不错——他估计下周就能完成、整篇论文将被完全形式化。但"它不是独自在推进，我在场"：他能读代码、看懂它做的每件事，能轻易发现并纠正问题，且相当频繁需要如此。典型问题：
有人本周建议：你抱怨 agent 不写足够一般的定理，是因为你让它"到达终点"、没让它"开发一个库"。但他认为问题比这更"近视（myopic）"：agent 在为项目开发工具时，只按项目第一个里程碑所需的受限方式来写，根本没意识到最终目标需要更一般的东西。很多（甚至大多数）此类问题可用 harness 缓解：让 agent 派生审查子 agent，审查一般性、对原材料的忠实性、避免重复等。但他这次刻意要"原味体验"——直接跑 Claude Code，看看拿到什么样的代码。
设想一个非常强的 agent（会跟证明、以正确一般性产出、很好），你于是让它形式化较复杂的东西，它产出 500,000 行代码。问题是：你怎么知道里面是什么？怎么知道能信任它？
信任是核心难题。你以为用了证明助手就没事——但它只检查定理的证明，不检查这些定理是否关于你想要的对象。也许你 50 万行的关键结果是"对象 A 在假设 H 下具有性质 P"，而 A、H、P 全是项目里新定义的、A 依赖 50 个环环相扣的新定义。Lean 只检查 P 是一个（有真假值的）性质，不检查 P 是不是你以为的那个性质。也许在很难察觉的地方，P 被定义成恒为真。而且"只要你逼得够狠，AI agent 能证任何东西"——每周 Lean Zulip 上都有人说自己证了 Riemann 假设或 Collatz 猜想（有时几个一起、在一个 500 行 repo 里），那是人坚持自己方法正确 + AI 极想给出肯定回答的产物：你拿一个错证明去坚持它对，最后就得到"P 被定义为 true"的代码。
因此我们需要事后建立信任的机制，而我们基本没有——这张幻灯片讲的全是"尚不存在的东西"。过去信任来自"把数学并入 mathlib"这一过程：论坛上人与人的长对话、有专家参与的长评审。若现在完全去掉这个过程、只用 AI agent，就需要事后工具来保证信任。可能方向（都还只是想法）：
但眼下没有能轻松提供这些的工具，所以你很大程度上必须亲自检查产出的代码——若你不懂 Lean 会很难。因此若想用 Lean 帮你信任 AI 合作者的输出，最好花几天亲手写点 Lean，至少能读懂你拿到的陈述。
最后一点：为获得 AI 加速，除"从库出发、建更好 harness 以避免重复劳动与技术债"外，一个很被低估的挑战是 AI 写自动化。他给出左侧同一命题的两个证明：证"两个可测函数的 (F+G)/2 也可测"——第一种显式串联引理（可测函数之和可测、除常数保持可测……）；第二种只调用一个别人写的程序，它能自动证一大类此类性质（可测性、连续性等在这类复合下保持的性质）。而我们从没见过 AI agent 自己写这样一个 tactic/程序来加速项目后续开发。AI 写自动化是真正应有更多投入的方向。