AI4Math · Invited Talk 02 · Leonardo de Moura

来源： Invited Talk 02 · Leonardo de Moura 播客： ICML 2026 · AI4Math 分类： AI 研究 原文发表： 2026-07-11 纪要生成： 2026-07-13

基本信息

• Workshop：3rd AI for Math Workshop — Toward Self-Evolving Scientific Agents
• 类型：Invited Talk（远程 Virtual）
• 题目：Machine-Checked Mathematics in the Age of AI（AI 时代的机器可检验数学）
• 讲者：Leonardo de Moura（AWS 自动推理组 Senior Principal Applied Scientist；Lean FRO 首席架构师与联合创始人；Lean、Z3、Yices 1.0、SAL 主要架构师；CAV/Haifa/Herbrand 奖、ACM 编程语言软件奖得主）
• 真实时段：约 09:00–09:32（KST，7/11）

一句话概括

以 Lean 为核心讲"AI 时代的形式化数学"：Lean 是可扩展（extensible）、可扩到大规模（scalable）、可信（trusted，靠多内核交叉验证）的证明助手，正让不懂形式数学的人也能借 AI 用上形式数学；而形式化的真正价值不止于"正确性"，更在于理解、沟通与可维护性。

开场：两个"百万行证明"故事点题

de Moura 用一个例子开场：去年，作者 Boris、Alexi 和 Dustin 解决了一个当时悬赏 1000 美元的开放猜想——他们本不太会 Lean，而是用 ChatGPT "vibe code" 配合 Lean 完成。他喜欢这个例子还因为：大约两周前，第一作者 Boris 又提交了约 100 万行代码的形式化——证否了"单位距离猜想（unit distance conjecture）"（一个开放约八年的问题）。对比之下：Boris 起初是 Lean 新手、几个月内从"用 Lean+ChatGPT 解一个开放猜想"到"提交百万行证明"，直观展示了 AI 时代形式化的速度。

主要内容

Lean 是什么：语言 + 证明助手

Lean 既是编程语言也是证明助手（Lean 本身用 Lean 实现）。同一系统里可写定义、写代码、写证明。三个核心特性贯穿全讲：

• 可扩展（extensible）：例如 mathlib（Lean 数学库）就有 5 万+ 行扩展；讲中会看到很多扩展例子。
• 可扩到大规模（scalable）：像 Boris 的证明这类是 10 亿行级别代码，必须可扩展。
• 可信（trusted）：可导出证明，交给独立检查器核验。

很多人把 Lean 当"游戏"（Kevin Buzzard 说 Lean 是他最爱的电脑游戏）：编辑器（VS Code / Vim / Emacs）右侧显示"游戏状态"（proof state）。

用一个例子演示"玩游戏"

以"证明：若 n 是奇数，则 n×n 也是奇数"为例：初始状态给定自然数 n，目标是该命题。

• 第一步 intro：引入"n 是奇数"这一事实；据奇数定义，存在 k，可命名为 k1。
• 还可给事实命名（如把"n = 2k+1"命名为 e1），并看到更新后的游戏状态。
• 下一步用最常用的"招"——simplifier（化简器）：告诉 Lean 展开奇数定义、用事实 e1（把 n 替换成 2k1+1，用等式到处展开）。
• 再用证明存在性的默认招：提供 witness（可为符号），最后用线性整数算术求解器收尾（做分配律、消项）。每个 tactic 变换目标直到无目标可证，最后 kernel 检查最终证明项。

kernel 会抓错：如果试图用 2 作 witness/ k 去"证明 3 是奇数"，检查会指出 3 ≠ 2×2+1。要点：你不需要信任我写的自动化，只需信任那个很小的 kernel。

信任来自"小 kernel + 多内核"

有人质疑小 kernel 是否有 bug——这不是问题，解决办法是多内核：由不同人、用不同编程语言、在不同硬件上实现。网站 arena.lean-lang.org 收集已提交的内核（如 nanoda，Rust 实现、很高效；有人还去优化 nanoda 并提交变体），用所有内核持续核验 mathlib，也可提交有挑战性的问题去暴露某些内核的 bug。核心思路：多内核提升你对"计算正确、你构造的证明正确"的信任。

Lean 生态现状与影响

• 规模：VS Code / Open VSX 上 250+ 唯一安装（未计 Vim/Emacs，因这些数据可从各自 marketplace 网站获取）；9000+ GitHub 用户在用。库不止数学（mathlib），还有物理、计算机科学的库；工业界 AWS、Google、Microsoft、Mistral 等在用。
• mathlib：既是定理集合，也是"形式数学仓库"（形式数学本质是"机器可检查的数学"）。700+ 贡献者、200 万+ 行，是众多项目的基础，例如：Kevin Buzzard 领衔的 Fermat's Last Theorem（费马大定理）项目只因 mathlib 才可能；AWS 关于差分隐私的验证项目也依赖 mathlib。
• Liquid Tensor Experiment：讲一段历史——2019 年 Fields 奖得主 Peter Scholze 为一个新结果"发狂"、想要形式版本；Johann Commelin 团队验证了证明、做了小修正，并且不仅验证还简化了证明。Scholze 视其为巨大成功，说 Lean 恰是帮他穿越"茂密丛林"的助手；成果登上 Nature。
• 其他项目：Carleson 定理已完成；Terry Tao 的 Equational Theories 项目探索大规模协作用 Lean；还有很多活跃的定理项目。名单最后一项他特别喜欢——当初曾说"某天 Lean 会用来判定 ABC 猜想"；Mochizuki 十多年前（约 2012）提交的 ABC 证明至今存争议，如今 Mochizuki 正在 Lean 里形式化其理论，把 Lean 当作"精确沟通思想的工具"——形式数学几乎成了让人们更好协作与沟通的工具。

形式数学的真正价值：可维护性 + 自动传播

形式数学更可维护：改定义后只需重建、看哪些证明坏了（仍能 type-check 的无需人工再验证）。相比 informal 数学，"AI 给出形式证明、人再检查是否正确"这一步在形式数学里可以跳过——你不必检查证明是否正确。他很喜欢 Ricardo Brasca 的一条消息：Brasca 庆祝有人推广了他们的结果，而且因为一切都是形式化的，这个推广被自动传播开来；对照"某人在 50 年前的论文里推广一个结果，你要如何追踪所有受影响的论文"——形式化里这是平凡的。

IDE 交互 + AI 助手 + 可读性

Lean 集成 IDE（如 VS Code）：右侧是 Info view（游戏状态）。直到最近多数用户把屏幕分两栏，如今很多人分三栏——底部是 AI agent 帮助形式化。AI 不只帮形式化，还能教你用 Lean：任何时候都能提问、让 AI 解释，它会"手把手"帮你上手。演示：用占位符（sorry，表示"暂不知道怎么证/稍后再做"）定义一个求和函数（0 到 m 的和），要证常见等式 2·Σn = n·(n+1)；问 AI，它很快返回证明，且附自然语言解释。形式数学是交互式的：可点击任意处看它在做什么——原来是按归纳法证明，base case 展示 2·(sum 0)=0·(0+1)、调用 simplifier；归纳步能看到归纳假设，可逐步执行（展开 sum 定义、化简、应用某条改写规则）；看到不懂的记号（如 _LHS、某分配律定理名）可点进去让 Lean/AI 告诉你。要点：证明是完全可交互的、不是静态对象；且读形式证明比写容易、读 Lean 比读 LaTeX 容易（可点击、可开任意证明、可问 AI 用自然语言解释）。

工具链：Verso、Blueprint、Lean Verbose、Workbench

• Verso：Lean 内嵌的领域特定文档语言（DSL），让你混排自然语言 / LaTeX / Lean；一个 Verso 文件就是 Lean 文件、在 VS Code 里有全部交互性。本次幻灯片就是用 Verso 做的——每个例子都正确（都经 Lean 检查、无笔误），所有动画由 Verso 计算生成（他说自己没耐心手做动画）。Lean 官网、他的个人主页也用 Verso 写；预期讲义、论文、各类文档乃至 doc-string 都会用 Verso。
• Blueprint：把 Verso 与 Patrick Massot 的 Lean Blueprints 结合成单一工具。Lean Blueprints 已用于许多项目（含 Liquid Tensor Experiment），能查依赖、当"建筑师"用；现在与 Verso 合并，帮助可视化并理解大型形式化项目，也能理解由 AI 完成的大项目——例如 sphere packing（球堆积）项目很大一块由 AI 完成，作者用 blueprint 理解 AI 做了什么。在 VS Code 里打开 Verso blueprint 可看到 LaTeX 混排 Lean、可悬停对象获即时反馈、依赖图自动计算（可见哪些已可形式化、哪些已形式化、哪些依赖缺失）。
• Lean Verbose：Patrick 做的另一工具，是"模拟自然语言的替代证明语言"，还提供点选（point & click）支持——给出建议、可选择、许多证明可仅靠点选构造，面向教育（有英文版，也有法文版）。最重要的信息是：Lean 可扩展——Patrick 无需与核心团队沟通，仅用 Lean API 就实现了这个工具（一个普通 Lean 文件）。
• Workbench（即将推出）：目标零安装——在浏览器里用 Lean/Verso/Blueprint、预配 AI，特别利于教学（无需让学生装 Lean、AI agent、MCP server/client），也能确保学生用正确/为课程定制的 mathlib 版本；对做 AI agent 的创业公司也好——很多公司的 agent 是 batch 模式（提交带 sorry 的 Lean 文件、返回证明），Workbench 能让它们轻松获得交互性，无需自建全部基础设施。

对 AI 的影响、TaoSet 与正确性保证

• 对 AI 的影响：每个在 IMO 拿奖且产出形式证明的系统都用了 Lean；许多创业公司（Mistral、Axiom、Harmonic、Math Inc、Logical Intelligence 等）在用。
• TaoSet：mathlib 由人维护，部分维护者对 AI 兴奋、部分不那么——他们想让 mathlib 保持"人类 curated"。两方都有道理。TaoSet（Kim Morrison 的想法）是一个地方：用 AI 做形式化的团队可存放并共享成果给其他团队；TaoSet 的路线图由人定，但代码由 AI 写、由 AI 审（Kim 做了很多用 AI 自动审查的 skills）。他特别兴奋的一点是偏微分方程（PDE）的部分支持——很多组在等 Lean 的 PDE 支持，AI 开始在此推进、加速需要 PDE 支持的团队很重要。TaoSet 网站已有 8 万+ 行，预计增长很快。
• Lean FRO：非营利，20 名工程师全职，不受任何公司控制，由 Sebastian 与 Leo 于 2023 年 8 月创立、即将三周年；至今 29 个 release、数千 PR，路线图公开。可扩展性是核心使命之一——mathlib 会变大很多（如 Boris 的百万行证明将提交到 TaoSet，会让它快速膨胀），他们持续改进 Lean 性能以应对 AI 产生的海量证明。
• 正确性关切：现在很多人用 Lean 证开放猜想，一个担忧是"是否证明了正确的东西"——Lean 检查的是"证明"、不检查"陈述是否正确"。为此，参考手册新增章节 "Validating a Lean Proof"，讲清用编辑器 / Lean Checker / 外部检查器各自能得到什么保证；还有相应博客。工具 comparator：对许多挑战问题，有 curated 版本的开放猜想陈述；若有人提交证明，可用 comparator 核验它是否真是该开放猜想的证明。例如 Boris 的"单位距离猜想为假"的证明（约 100 万行）就提交到 linlang / leanlang.vol 相关网站，并用 comparator 核验（已有 curated 版陈述，comparator 有 web 版、无需本地安装，可选不同内核）。comparator 的工作方式：可为每个问题创建"challenges"——带占位符（sorry，可在定义位置）的问题，让 AI 合成证明乃至定义，用 Lean kernel 检查结果、可选内核。Kim 写的 LeanVal 网站收录大量难度不一的挑战题（共 211 题，从很易到极难；短期内不指望 AI 全解），各组提交（相信是 AI 生成的）解——因为像单位距离猜想那样的百万行证明，人手写要花数月，是"疯狂的工作量"；任何人都可提交新问题。

关键结论 / Takeaways

• 形式化不只是"确保正确"，更是理解、沟通、驾驭超出认知容量的结构；AI 让不懂形式数学者也能受益（甚至用 ChatGPT vibe-code 解开放猜想）。
• 信任建立在小 kernel + 多内核交叉验证（arena.lean-lang.org、nanoda）之上；证明可读、可交互、可让 AI 讲解，读比写容易、读 Lean 比读 LaTeX 容易。
• 可维护性带来"泛化自动传播"；Lean 高度可扩展的工具链（Verso / Blueprint / Verbose / Workbench）+ mathlib / TaoSet 正支撑 AI 规模化形式化。
• 用 Lean 证开放猜想时要分清"证明被验"与"陈述正确"：靠 "Validating a Lean Proof" 章节、comparator、多内核、LeanVal 题库来保证。

Q&A / 讨论亮点

• Q1（一位 AI for math 方向的学生）： Lean 里有没有"设计时没料到、却对 AI 时代协作很有帮助"的东西？ A1： 在持续改进工具、也在为"帮助人开发 AI"做工具。例如 Lean FRO 在开发 Lean 的 MCP（"Lean being"），希望未来成为标准——这很重要，因为 AI 实验室会据此训练，最好有一个"自带 Lean 保证"的 MCP、对每个 Lean 用户都可用；配合 Workbench 加速开发。另一件事是证明自动化（本讲没细讲）：他们努力让自动化行为像"白盒"，可由 AI 和人共同控制——通常基于可满足性/模理论的自动化是黑盒，但 Lean 里做成白盒，让 AI 能控制其行为；希望 AI 能在更高抽象层使用这些自动化。

• Q2（一位业余做 AI for math 的工程师）： 你觉得 Lean Verbose 能用来教 LLM 更擅长 Lean 吗？ A2： 不认为那是 Lean Verbose 的主要目标；它的目标是教育。如果想造一个帮学生学数学的 AI，能看到价值；但若目标是"用 AI 证开放猜想或做程序验证"，Lean Verbose 并非为此优化——它面向教育，AI 在其中可帮助教学、辅助使用 Lean Verbose 的学生。（随后主持人致谢，de Moura 结束。）

名词 / 引用

• Lean / mathlib / kernel：证明助手兼语言、数学库、可信小核。
• nanoda / arena.lean-lang.org：Rust 实现内核 / 多内核收集与挑战站。
• Liquid Tensor Experiment：Scholze 结果的形式化（Commelin 团队，登 Nature）。
• Fermat's Last Theorem 项目（Buzzard）/ Carleson 定理 / Equational Theories（Tao）/ Mochizuki 形式化 ABC：mathlib 之上的重要项目。
• Verso / Lean Blueprint / Lean Verbose / Workbench：Lean 工具链（幻灯片本身用 Verso 做）。
• TaoSet：AI 形式化成果共享库（路线图人定、代码 AI 写与审；PDE 支持推进中；8 万+ 行）。
• comparator / LeanVal（211 题）/ linlang·leanlang.vol：证明核验工具、挑战题库、提交站。
• unit distance conjecture：Boris 提交约 100 万行证否，经 comparator 核验。
• Lean FRO：2023/8 创立、20 全职、29 release、数千 PR，非营利。

原文发表：2026-07-11  ·  纪要生成：2026-07-13