主题演讲

Leonardo de Moura：Lean——作为 AI 与科学基础设施的机器验证证明

Leonardo de Moura: Lean: Machine-Checked Proofs as Infrastructure for AI and Science

主题演讲🎤 莱昂纳多·德·莫拉 (Leonardo de Moura)⏱ 14:13👁 NA

▶ 在 YouTube 观看

Lean 的创造者 Leonardo de Moura 阐述 Lean 如何把数学变成可机器验证的「数据」，并成为数学研究、软件验证与 AI 的可信基础设施。

核心要点

Lean 把证明变成一个有「招式」的游戏（引入假设、化简、求解算术等），AI 已学会玩这个游戏，而 Lean 最重要的价值是能即时抓出人的错误并给出反馈。
Lean 已被广泛采用：仅 VS Code/Open VSX 安装就超 10 万次，GitHub 上有 9000+ 含 Lean 代码的仓库，被 AWS、Google、Microsoft、Mistral 等公司使用。
数学库 mathlib 由 700+ 贡献者建成、超 20 万条定理，让数学变成可被研究、可视化和自动转换（如自动生成依赖图）的「数据」。
标志性的「液态张量实验」(Liquid Tensor Experiment) 证明了 Lean 能作为顶级数学家（菲尔兹奖得主 Peter Scholze）的可信「助手」，甚至帮助简化了证明。
Lean 已超越数学，进入软件验证：AWS 用它验证权限/访问控制（Lean 模型比 Rust 实现小 10 倍且更快），Microsoft 用它验证密码学，Google 用它验证 JPEG 代码。
2024 年初业界普遍认为 AI 不可能在 IMO 拿奖，如今多支团队已借助 Lean 等工具获得 IMO 奖牌乃至满分，标志着 AI 数学能力的快速突破。

分章详解

把证明变成一场游戏：Lean 的核心交互

以「若 n 是奇数则 n 的平方也是奇数」为例，演示证明如何像棋局：先引入假设（存在 k 使 n=2k+1），再走下一步招式。
「化简器」(simplifier) 是最常用的招式，在 Lean 数学库中被使用超过 10 万次；其后用存在量词的标准证法给出 k，最后交给线性整数算术求解收官。
AI 已学会玩这个游戏，而大多数用户每天都在玩它。
Lean 最关键的作用是抓错：若用错误的见证值（如声称某数等于 2×2+1）证明奇数，Lean 会立即指出矛盾并给出反馈。

可独立验证与开放生态：Arena 与采用规模

证明可由独立的检查器 (checker) 核验；社区设有名为 Arena 的平台，让业余者、专业人士和开发者贡献自制的内核来检查数学库。
采用规模庞大：仅 VS Code 与 Open VSX 上就有十万级别的安装量。
GitHub 上有超过 9000 个含 Lean 代码的仓库，涵盖最大的数学库 mathlib，以及新兴的物理学、计算机科学库。
被 AWS、Google、Microsoft、Mistral 等公司实际使用。

数学即数据：mathlib 与形式化数学

形式化数学就是机器可验证的数学；mathlib 由 700 多位贡献者建成，包含超过 20 万条定理。
一旦数学被形式化，它就变成可被研究、可视化和转换的「数据」。
例如有人选取一个 Lean 项目后，依赖关系图就能被自动生成——因为数学现在是数据。

液态张量实验与数学家的信任

2019 年，菲尔兹奖得主 Peter Scholze 把他自认为职业生涯最重要、令他「快要发疯」的证明抛给 Lean 社区挑战——这发生在 AI 之前，纯靠人力完成。
社区不仅验证了证明，还在并不完全理解证明的情况下将其简化；Scholze 说自己当时只能看到两步之远，正是因为有 Lean 才得以完成。
Scholze 把整个项目总结为：Lean 正是一个「助手」，在形式化中提供协助。
另一位菲尔兹奖得主（2022 年获奖）也开始使用 Lean，并视其为一种「沟通工具」，它改变了用户的协作与互动方式。

超越数学：软件与系统验证

AWS 的 Verified Permissions 与 Verified Access 的模型用 Lean 编写并开源；针对 Rust 程序的 Lean 模型体积小 10 倍，测试中 Lean 在此类应用上甚至比 Rust 更快。
Microsoft 用 Lean 验证密码学：将 Rust 翻译成 Lean，再由验证工程师用 Lean 完成验证。
约两周前有团队报告，自主生成的（密码学）代码比专业开发者更快。
Google 也在用 Lean 验证 JPEG 相关代码。

AI 时代的里程碑与项目治理

10 年前演讲时讲者就预言 Lean 终有一天能帮助 AI；如今 AI 数学能力突飞猛进。
2024 年初业界普遍断言 AI 不可能在 IMO 获奖，如今多支团队已斩获 IMO 奖牌，初创公司在解决开放问题、在基准测试中取得满分。
Lean 不再是研究项目，而是社区要求达到高质量的产品：自 2023 年 Sebastian 发布以来已有 29 个版本、8500 多个合并请求，路线图公开。
项目不受任何单一公司控制，依赖工程师社区与慈善捐赠支持；讲者坚信 AI 将改变我们做数学的方式。

关键引述

“最重要的部分是 Lean 能抓出你的错误——你会立即得到反馈，并能验证你的证明。（the most important part is Lean catches your mistakes... You get immediate feedback and you can check your proofs.）”— Leonardo de Moura

“在形式化数学中，数学变成了可以被研究、被以多种方式可视化、被转换的数据。（in formal mathematics mathematics becomes data that can be studied, can be visualized from many different ways and transformed.）”— Leonardo de Moura

“Peter Scholze 把整个项目总结为：Lean 正是这样一个东西——一个在形式化中提供协助的助手。（Peter summarized this whole project saying that Lean was exactly that, an assistant.）”— Leonardo de Moura（转述 Peter Scholze）

“Lean 已不再是一个研究项目，社区要求它成为高质量的产品。（Lean is not a research project anymore; the community demands it to be a high quality product.）”— Leonardo de Moura

术语 / 人物

Lean — 由 Leonardo de Moura 创建的开源证明助手与编程语言，用于编写机器可验证的形式化证明，现也用于软件与硬件验证及 AI 数学。

mathlib — Lean 的统一数学库，由 700+ 贡献者建成、含 20 万+ 定理，是目前最大的形式化数学库。

Liquid Tensor Experiment（液态张量实验） — 2019 年 Peter Scholze 向 Lean 社区发起的形式化挑战，成功验证并简化了他的关键定理，是 Lean 进入主流数学界的标志性事件。

Peter Scholze — 德国数学家，2018 年菲尔兹奖得主，凝聚态数学的提出者，液态张量实验的发起人。

Lean FRO — Leonardo de Moura 与 Sebastian Ullrich 共同创立的非营利「聚焦研究机构」，负责维护并推进 Lean，使其更可扩展、易用和高质量。

simplifier（化简器） — Lean 中最常用的证明自动化策略，用于自动化简表达式，在 mathlib 中被使用超过 10 万次。

SMT / Z3 — Z3 是 de Moura 创建的著名 SMT（可满足性模理论）求解器，是自动推理领域的核心工具之一。

背景补充

Leonardo de Moura 是巴西裔计算机科学家，Z3 SMT 求解器与 Lean 证明助手的创造者。他于 2013 年在微软研究院创建 Lean，在微软任职 17 年后于 2023 年加入 AWS，现任自动推理组高级首席应用科学家，同时是 Lean FRO 的联合创始人兼首席架构师。他曾获 2021 年计算机辅助验证奖、2025 年 ACM SIGPLAN 编程语言软件奖等多项荣誉。本视频是其在 SAIR（陶哲轩等联合创立的科学与 AI 研究基金会）相关活动上的主题演讲。

适合谁看

适合关注 AI 辅助数学、形式化证明与软件验证的研究者、数学家、工程师，以及想了解 Lean 生态与「数学即数据」理念的科技从业者与决策者。