2026年8月1日，OpenAI宣布其未发布的下一代模型Astra在10个悬而未决的数学和理论计算机科学问题上取得了新结果，涵盖高维几何、编码理论、群论、算子代数等8个领域。每一个结果都附带了可以被机器逐行检查的Lean 4证明证书，发布在GitHub上，任何人用一台笔记本电脑就能独立验证。
这里反复出现的"Lean"，是一门大多数开发者和数学爱好者可能只在新闻里见过名字的编程语言。简单说，Lean既是一门编程语言，也是一个证明助手。你可以在里面写代码，也可以写数学证明，而且Lean会替你检查证明是否正确。它的独特之处在于：你写的证明不是给人看的文字论证，而是一段可以被计算机严格验证的程序。如果Lean说你的证明通过了，那就意味着这个结论在数学上成立，没有任何模糊地带。
就在OpenAI发布这些成果后不到十天，播客The Peterman Pod的主持人Ryan Peterman对话了Lean的创造者Leonardo de Moura。de Moura目前在AWS担任高级首席应用科学家，同时是Lean背后的非营利研究组织Lean FRO的首席架构师和联合创始人。他也是另一个广泛使用的工具Z3 SMT求解器的创造者。在这次对话里，他说："我已经不再写测试了。我写性质，然后AI替我证明。"
1. 测试能找到bug，证明能消灭bug
de Moura用计算机科学家Dijkstra的一句话开场："程序测试可以用来表明存在bug，但永远不能证明bug不存在。"
这句话是理解Lean存在意义的钥匙。一个测试套件无论多全面，覆盖的终究是你想到的场景。总有某个边角情况不在其中。形式化证明做的事情不同：它覆盖所有可能的场景，给出数学意义上的保证。
一个具体的例子：想象程序里有一排格子，一共10个，编号从0到9，这就是一个数组。程序需要从某个格子里取数据，用一个叫i的变量记录"取第几个格子"。如果i跑到了10或者更大，程序就去取一个不存在的格子，这就是越界访问，轻则数据出错，重则系统崩溃。
在C语言里，编译器不会拦你，只有程序跑到那一行的时候才会出事。在Lean中，你可以写一条数学语句，声明在程序的某个位置，索引变量i的值大于等于0且小于10。Lean会要求你证明这条语句为真。证明不了，代码就过不了检查。问题在写代码的时候就必须解决，你得向Lean交代清楚"为什么i不会越界"。
验证过程会用到一种叫霍尔三元组的技术，它把每条语句拆成三部分来推理：执行前什么条件应该为真、语句本身做了什么、执行后什么条件保证为真。自动化工具会处理大量这样的推理步骤，让证明可以模块化。de Moura把这个过程比作在源代码上方叠加了一层"第二个软件层"，专门用来描述和验证程序的行为。
但Lean本身的程序怎么办？如果连Lean自己都可能有bug，凭什么信任它的验证结果？
2. 5000行代码，多个独立内核，零信任架构
de Moura的回答里有一个清晰的分层：你不需要信任整个Lean，只需要信任它的内核。
在Lean中，证明检查本质上就是类型检查。你写了一个证明项，Lean的内核检查这个项的类型是否匹配你声称要证明的命题。这个内核只有大约5000行代码，目标是小到任何人都能自己从头写一个。
Lean本身是一个庞大的程序，功能在不断增加，很难给出完整的规格说明。但内核可以有精确的规格说明，而且已经有人这么做了。Mario Carneiro用Lean本身写了一个叫Lean4Lean的内核，并证明了它相对于Lean语义的正确性。还有人用Rust和其他编程语言实现了独立的内核。
拥有多个独立内核是确保结果正确的最好方式。 一些外部内核还会打印出所有已证明命题的完整列表及其依赖链。这样你可以确认自己看到的确实是你想证明的东西，而不是某个无关的恒真式（比如2+2=4）被冒充成了你的定理。
如果要验证的是用C或Rust写的软件呢？有两条路线。第一种叫浅嵌入（shallow embedding），把目标语言翻译成Lean，然后验证翻译后的版本。现在已经有工具Aeneas可以把Rust代码映射成Lean。第二种叫深嵌入（deep embedding），在Lean里写出目标语言的语义，程序变成Lean里的数据结构，可以对这个数据结构声明性质并证明。
3. Kim Morrison用一周做到了过去要几个月的事
de Moura的同事Kim Morrison最近做了一件他几个月前还认为不可能的事。
她用AI把C语言的压缩库zlib翻译成Lean，确保翻译版通过了zlib的测试套件，然后证明了一条关键性质：压缩数据再解压，一定能恢复原始数据。 对一个压缩引擎来说，这可能是最重要的性质了。
整个过程用了大约一周。Kim Morrison的GitHub仓库lean-zip显示，实现和验证都由松散监督的AI完成，底层包含超过1100条定理、约32000行证明代码，没有任何未完成的占位符，每次提交都会从头重新检查所有证明。
现在他们在让AI优化代码，但有一条硬约束：优化不能破坏已有的证明。这正是de Moura反复强调的一个核心观点：有了证明，优化就是免费的。 你不需要人工检查优化后的版本有没有引入bug，因为证明会替你守住所有性质。
这件事之所以重要，是因为它改变了形式化验证的成本结构。
de Moura给了一个直觉：如果写程序花x时间，过去做形式化验证要花10x。但真正的痛苦在于维护，而非初始投入。程序在不断变化，每次改动都可能破坏证明，就像改了代码后测试全红一样，只是修证明比修测试更难，因为你可能已经不记得某个证明背后的逻辑了。
AI在这个环节表现极好。de Moura举了自己前一天的经历：他想修改一些他本人没写的证明，甚至不知道那些证明是关于什么的，他告诉AI"请在不使用某个特性的情况下重写这些证明，因为我要改动它"，AI瞬间给出了新版本。
"I used to believe my superpower was that I could tolerate a lot of pain. That superpower is no longer relevant." 他在另一场演讲中这样总结。
作为对比，seL4是AI出现之前形式化验证的标杆项目。这个经过完全验证的微内核只有大约8700行C代码，验证总共花了约20人年的工作量，每行代码的验证成本约350美元。AWS过去十年一直在用形式化验证，但只敢用在最关键的安全组件上，因为成本太高。
AI改变了这个等式。规格说明你仍然需要人来写，但它从来不是最痛苦的部分。最痛苦的是手工开发证明和维护证明，AI在这两件事上都极其擅长。
4. 一个低效的程序本身就是最好的规格说明
"那规格说明是不是比测试套件难写得多？"主持人问。
de Moura给了一个否定的回答。很多时候，开发者心里清楚程序应该满足什么性质，只是过去没有工具让他们表达并验证。 现在流行的property-based testing就是在做这件事：开发者写下期望成立的性质，用随机输入去检验。形式化验证是这条路的终点：同样的性质，不用测试，直接证明，覆盖所有可能的输入。
然后他提出了一个更关键的观察：一个低效的程序本身就可以当规格说明。 你可以用最朴素、最慢、最容易理解的方式写出"我想要什么"，然后让AI生成高效版本，并证明高效版本与朴素版本等价。
这消除了"规格说明太难写"的顾虑。写一个低效的正确程序通常远比写一个高效的程序容易，因为高效版本里充满了你不敢随便改的巧妙技巧。有了证明，你可以让AI放手优化，因为任何优化都必须通过"和朴素版本等价"这道关卡。
5. IMO金牌、Fields奖得主的求助、100万行证明
Lean在数学领域的突破比软件验证更早引起公众注意。
2024年，DeepMind的AlphaProof用Lean获得国际数学奥林匹克（IMO）银牌。当时整个社区觉得这已经是了不起的成就。到2025年，Harmonic的Aristotle系统、ByteDance的Seed-Prover都用Lean的形式化证明拿到了金牌水平。de Moura说他几年前认为在IMO拿金牌不可能，"现在大家把它当作简单问题的基准"。ByteDance参与这件事尤其让他意外：他之前不知道TikTok背后的公司有一个形式化数学团队。
AI把Lean当成一个游戏来玩。Lean有一种叫tactic模式的证明书写方式，输入一个"by"关键字就进入这个模式。用户在这种模式下逐步对证明状态施加变换，比如"简化当前目标""应用某条已知规则"，每一步操作后屏幕右侧的info view会立刻刷新，告诉你还剩什么需要证明。目标是让"剩余目标"归零。AI通过强化学习不断尝试步骤，观察状态变化，就像下棋一样。有用户告诉de Moura："你给我造了我最喜欢的电脑游戏。"
更早的一次标志性事件发生在2020年。Fields奖得主Peter Scholze有一个他自己都不确定是否正确的结果，这是他认为自己职业生涯中最重要的成果之一，但他一直没有发表，因为没有十足把握。他把它交给Lean社区，由Johan Commelin领导的团队完成了形式化验证，还在不完全理解证明的情况下简化了它。
de Moura把这比作代码重构：你开始修改代码，程序变快了，但你不完全理解为什么。团队有直觉，有info view的持续反馈，一步步推进。这个项目让数学界意识到形式化是一种强大的协作工具：你不需要信任别人的证明，他们可以为你填补空白，Lean的内核会替你检查一切。此后，Fields奖得主陶哲轩（Terence Tao）也开始使用Lean。他第一次用完说"我大概不会再用了"，一周后就开了第二个项目。
2026年5月，OpenAI宣布其模型反驳了Erdos的单位距离猜想。Kim Morrison随即在Lean社区的挑战平台上发布了形式化挑战。OpenAI的Boris Alexeev用Sol模型完成了完整的形式化，整个证明（含所有依赖库）约100万行代码，从挑战发布到完成大约两周。de Moura强调，这个底层需要的数学基础设施（代数数论等内容）在过去需要专家花几个月手动形式化。到8月1日，OpenAI的Astra模型又把这个范式推得更远：10个横跨8个领域的开放问题，每一个都带Lean 4证明证书。
但de Moura对AI在数学中的能力边界说得直接：AI可以找到已有问题的新证明路径，可以反驳猜想，但还没有证据表明它能提出新的数学概念。 Lean社区的挑战平台上有一些要求AI自己构造数学对象的题目，这仍然处于能力边界。他不愿意打赌说AI永远做不到，但截至目前，证据还没有。
6. 同一个人造了Z3和Lean，为什么需要两个
de Moura在创建Lean之前，花了近20年时间打造Z3 SMT求解器。Z3是一种可满足性模理论求解器，可以理解为增强版的SAT求解器，在布尔逻辑之上加了对算术、数组等理论的支持。你可以把一个数独问题编码成一组约束扔给Z3，它会瞬间给出答案。
Z3和Lean都被归类为定理证明器，但它们完全不同。Z3是全自动的、推按钮式的：你给它一组约束，它要么说"不可满足"（意思是不可能），要么给你一个反例。用户无法控制Z3的推理过程。Lean是交互式的：用户或AI可以逐步控制证明的每一步。
Z3在找bug方面非常成功。比如你知道程序里有一条路径存在安全漏洞，但不知道什么输入能触发它。把这条路径转化成约束集合扔给Z3，Z3会告诉你：要么这条路径不可达（你安全了），要么给你一组具体输入说"用这个就能触发"。
但对于证明bug不存在，Z3不够用。一旦性质涉及全称量词和复杂前后条件，Z3的启发式规则就会失败或超时。de Moura在这里做了一个区分：程序和硬件之所以正确，原因通常很简单，没什么深奥的，这就是为什么自动化工具在实际的硬件验证和有界检查中效果很好。 但一旦要证明通用性质，问题变成不可判定的，自动化工具就力不从心了。
Lean诞生的直接原因就是这个局限。
另一个致命问题是"证明不稳定性"。de Moura提到一位Amazon同事的工作：用Z3类的自动化工具维护证明时，仅仅把公式A∧B改写成B∧A就可能导致证明失败。你什么实质内容都没改，只是调换了两个条件的顺序，证明就崩了。在Lean中，因为用户（或AI）控制着证明的每一步，这个问题消失了。那位同事切换到Lean之后，维护体验"super smooth"。
AI在这里带来的惊喜是：过去只有人类能分步骤解释"为什么某件事是对的"，现在AI也能做到。它可以一步步说服Lean某件事成立，提供完整的证明项。Z3只能给你一个结论（行或不行），Lean可以给你整条推理链。
7. 数学家说：没有依赖类型，我们不玩
Lean在设计之初面临一个根本选择：用高阶逻辑（higher-order logic）还是依赖类型理论。高阶逻辑实现起来简单得多，de Moura最初倾向于这个方向。
Carnegie Mellon的哲学与数学科学教授、Lean早期核心贡献者Jeremy Avigad说服了他。Avigad的论点是：如果想吸引Fields奖级别的数学家，高阶逻辑行不通。高阶逻辑适合具体数学，但处理抽象对象时必须用编码技巧来模拟，结果一团糟。de Moura说他跟陶哲轩、Kevin Buzzard、Patrick Massot等数学家交流时，没有一个人认为高阶逻辑够用，"None. I mean, you talk to Terence Tao, Jeremy, Kevin Buzzard, Patrick Massot, they would say, 'No, no, you have to do the dependent type theory.'"
依赖类型的核心思想可以用一个例子说清楚。假设你有一个结构体，里面有字段x和y都是整数。在依赖类型理论中，你可以加第三个字段，它的类型是"x > y的证明"。这意味着你不可能构造这个结构体的实例，除非你同时提供x确实大于y的证据。不变量直接嵌入类型系统，不需要额外发明。
这在函数签名里也一样。一个除法函数可以要求调用者提供"除数不等于零"的证明。没有这个证据，函数就无法被调用，不是运行时报错，而是编译时就过不了。
过去人们嫌提供这些证明太烦。但AI出现后，情况变了：AI可以自动合成这些类型层面的证明。 依赖类型理论从"理论上优美但实践中烦人"变成了"理论上优美而且AI替你做烦人的部分"。
de Moura说，这是他从用户那里学到的最重要的教训之一。听用户说什么，比坚持自己的技术偏好重要得多。 如果你想吸引某个社区，你必须提供他们真正需要的东西。说"高阶逻辑对数学也够用"在技术上或许有道理，但数学家们不这么认为，这就够了。
8. 编译成功的那一刻，他差点哭了
Lean有一个特性，在编程语言中不多见：它的所有工具链都用Lean自身实现。编译器、构建系统Lake、文档系统Verso、LSP服务器，全部是Lean代码。这叫自举（self-hosting），从C++切换到Lean自举的过程是de Moura职业生涯中最痛苦的技术挑战。
大约10万行代码需要用Lean自身的最基础特性重写。你从第一个文件开始编译，失败了，修bug，编译通过，第二个文件又失败了。整个过程就是不断发现新旧实现之间的差异并逐个解决。Lean的依赖类型系统意味着某些基础证明你必须手动构造，没有任何交互工具帮忙，几乎像是在写汇编语言。
当他终于成功编译了Lean的那一刻，他说自己差点想哭。 他打电话给联合创始人Sebastian Ullrich说"Wow, man. This is insane."问Sebastian激不激动，Sebastian说"Yes, I am. I am." 很多人认为他们不可能完成这件事。
但自举带来的回报是极端的可扩展性。因为Lean的所有组件（解析器、宏系统、编译器、策略框架）都是Lean代码，用户可以用同一门语言去操作和扩展这些组件。你可以在写数学证明的过程中，在同一个文件里写一段元程序来自动化某个步骤。AI也会利用这一点：如果你让AI调试一个Lean文件，它会自己写Lean元程序来验证它关于问题原因的猜想。de Moura说看到这种行为时觉得"crazy"。
这种可扩展性产生了一些令人意外的项目。Patrick Massot是巴黎-萨克雷大学的数学家，不是计算机科学家。他用Lean的扩展机制创建了Verbose Lean，一种用受控自然语言（英文或法文）写证明的教学系统，还加入了点击式界面，学生可以点击屏幕上的选项来推进证明，看上去完全像一本教科书。他完成整个项目没有问过de Moura任何问题。
类似的例子还有协议验证领域的Veil，它在Lean之上嵌入了一套协议验证专用语言，打开后感觉像是一个完全不同的系统，但底层只是一个带扩展的Lean文件。开发团队唯一一次联系de Moura是说"能不能让Lean的某个环节跑快一点"。
在工业端，Lean作为编程语言的最大规模实践在AWS内部：一个用于AI加速器的编译器，50万行Lean代码。这个项目主要把Lean当编程语言用，顺带证明一些程序性质。de Moura把这些证明叫做"bonus"：你不是为了证明而写Lean，你是为了写程序而写Lean，但证明这件事自然而然就可以做了。
在数学一侧，Lean的数学库Mathlib是目前最大的形式化数学库。要陈述一个开放猜想，你需要库里有相应的概念定义。比如IMO的题目用到实数，Mathlib里有实数的完整定义。Mathlib目前距离覆盖现代研究级数学的全部定义只差不到1000个。
社区也是竞争力的一部分。在AI普及之前，用户在Lean的Zulip聊天频道提问，通常五分钟内就能得到答案。de Moura引用有人开玩笑说的"human-based AI"来形容这种响应速度。Lean的早期核心用户Jeremy Avigad曾经跟de Moura说：任何他请求的新功能，当天就能拿到。 这种响应速度是社区增长的重要原因。
9. "写代码是有趣的部分，把它变成产品从来都不有趣"
de Moura对Lean和形式化验证的未来给了三个判断。
第一，数学验证和软件验证的技术挑战方向相反。 在数学中，声明通常简短，但证明可能极长极深。Erdos单位距离猜想的反例就是这样：问题本身一句话就能说清楚，但证明要100万行代码。在软件验证中，规格说明往往庞大（因为程序复杂），但每一条性质的证明通常浅，因为程序正确的原因大多不复杂。Lean需要在可扩展性上同时满足这两个方向。
第二，大型AI实验室认真训练Lean是最近的事。 在此之前，Lean只是"碰巧在数据集里"，没有针对性的强化学习管线。现在看到的成果已经令人惊叹，但未来会好得多。de Moura预测，Lean和同类型的语言（比如Rocq）会因此变得更主流。很多人过去说"函数式编程我不喜欢"，但如果大部分代码都不是你自己写的，代码长什么样其实不重要，重要的是规格说明层面的表达力。
第三，手写数学不会消失，但混合工作流会成为常态。 de Moura用了一个比喻：就像有了机器制造家具之后仍然有人喜欢手工打磨，手写证明作为沟通和教学工具会继续存在。但完全不在工作流中使用AI的人会越来越少。
他自己已经不写测试了。"I'm not writing tests anymore. I'm writing properties and proving them. The AI is proving most of them for me." 他觉得"写代码"这件事里，有趣的部分是原型设计，尝试新想法。把原型变成产品从来都不有趣。AI可以接管这些不有趣的部分，没有人真正喜欢做那些事。
人类在这个未来中的角色是写接口：告诉AI我们想要什么（规格说明），理解AI生成的数学库中的抽象，确保整个系统与现实世界的需求对齐。规格说明会一直存在，人类会一直在那个界面上。
他给想学Lean的人的建议是直接跟AI对话。很多人现在把屏幕分成三块：Lean代码、info view、底部的AI智能体。AI在写代码的同时用自然语言解释发生了什么。陶哲轩早期学Lean时还是手动在ChatGPT窗口和VS Code之间复制粘贴，现在有了AI智能体效率更高了。lean-lang.org上有多本入门书籍，包括函数式编程、定理证明和数学三个方向。
被问到如果能回到过去给自己一个建议会说什么，de Moura笑着说他宁愿保密。"Ignorance is a bliss." 不知道事情有多难，反而敢开始。不过他还是给出了一条：我是个极度内向的人，我会告诉年轻时的自己，练好跟人打交道的能力。 当你要跟一个社区互动的时候，这比你以为的重要得多。
核心问答
Q1: Lean到底是什么，跟普通编程语言有什么区别？Lean是一门编程语言，同时也是一个证明助手。你可以用它写程序，也可以用它写数学证明，而且Lean会自动检查你的证明是否正确。跟普通编程语言的关键区别是：Lean基于依赖类型理论，类型可以依赖于值，这意味着你可以在类型签名里直接表达"这个函数的输入必须满足某种条件"这样的约束，编译器会在编译时强制你提供证据。这让"写出有bug的程序"在某些情况下变得不可能，因为类型检查通不过。
Q2: AI在形式化验证中到底解决了什么问题？解决的是证明的开发和维护。规格说明（你想要程序满足什么性质）仍然需要人来写，但它从来不是最痛苦的部分。最痛苦的是手工构造证明和在代码变动时修补证明。seL4微内核的验证花了20人年，主要成本在这里。AI可以在几秒内完成同类任务，而且质量稳定。Kim Morrison用AI在一周内完成了zlib压缩库的翻译和关键性质证明。这把形式化验证的成本从"10倍于写程序"降低到可能接近写测试的水平。
Q3: de Moura同时创造了Z3和Lean，这两个工具有什么本质区别？Z3是全自动的约束求解器：你按一个按钮，要么得到答案，要么超时，无法控制推理过程。它擅长找bug（给一个路径，问能不能走到），但证明bug不存在时经常失败或超时。Lean是交互式的：用户或AI可以逐步控制证明的每一步。Z3还有一个"证明不稳定性"的问题：仅仅调换公式两个子句的顺序就可能导致证明失败。Lean因为每一步都是显式的，没有这个问题。Lean诞生的直接原因就是Z3在证明软件正确性方面的局限。
