AI 会写证明，谁来检查？Leonardo de Moura 谈 Lean 的可信基础与 AI 时代的形式化工程

一、嘉宾背景

Leonardo de Moura 在这期节目中的身份不是旁观评论者，而是 Lean 生态的核心建设者。他被介绍为 Lean 的创造者、Lean FRO 的 chief architect 和 co-founder，同时也是 AWS 的 senior principal scientist。Lean FRO 在材料中被描述为 Lean 背后的非营利组织，而本期讨论的对象正是 Lean theorem prover、核心系统、扩展机制、Mathlib 社区和形式化证明验证。

节目标题“AI Can Write the Proof. Who Checks It?”准确概括了访谈的张力：AI 已经能参与证明生成、代码迁移和证明维护，但当 AI 产物越来越长、越来越难读，甚至可能利用检查器漏洞时，谁来检查 AI？因此，这不是一集泛泛讨论 AI 数学能力的节目，而是一场关于 Lean 可信基础、kernel 安全、开源治理、形式化软件工程和 Mathlib 规模化的系统分析。

de Moura 也在访谈中澄清了自己与 Lean 核心的关系。他说，Lean 的核心系统现在并不是由他个人控制；Lean FRO 大约有 20 人，开发者分别拥有系统的不同部分，并对是否接受外部请求作出决策。这一点重要，因为整集节目不断回到同一个主题：可信系统不能靠一个天才维护者的个人权威维持，而要靠明确的所有权、透明的检查机制、可扩展的社区边界和不断缩小的可信代码基来维持。

二、本期主要内容

访谈的第一条主线，是 Lean 核心系统为什么需要接近 cathedral model 的治理。de Moura 说，给库贡献和给核心系统贡献不是一回事：一个二叉树库缺少若干函数或定理，仍然可以有用；但核心系统的组件高度互联，缺口、崩溃和半成品功能都会影响整个系统。他列出随机合并核心 PR 的风险：引入 bug，留下看似可用但并未完成的功能，锁死未来设计或优化路径，让团队优先级变得混乱。他还回忆曾把 Slack 里只抛想法、不写有用代码的人移出，只留下真正贡献代码的核心成员。

但 de Moura 的“核心保护”并不等于封闭。他强调，Lean 被设计成可扩展系统，社区可以在不修改核心、不和核心团队协调的情况下构建 DSL 和工具。节目中提到的例子包括面向分布式协议的语言，以及 Ilse Sergey 和学生展示的用于软件验证的 Lean 扩展。Lean 4 的变化进一步强化了这个方向：系统用 Lean 实现 Lean，Lean 文件可以访问内部表示，AI 和 autoformalization 团队因此能直接抽取 Mathlib proofs 的训练数据，Velvet、Veo 等工具也建立在这种可扩展性上。

第二条主线，是 Collatz 相关事件带来的安全警报。事件中，有人提交了一个声称被官方 Lean kernel 和外部 Rust checker Nanoda 接受的证明或反证明。团队调查后认为，它分别利用了官方 kernel 与 Nanoda 中完全不同的 bug，并强烈相信它是 AI 构造的。de Moura 的判断不是简单地说“AI 可能犯错”，而是更严厉：AI 很擅长耐心做低层实现搜索，反复触碰人类不愿长时间钻研的角落，从而找到 soundness bug。

由此，访谈把“谁检查 AI”推进到工程层面。de Moura 反对隐藏私有 kernel，认为 Lean 社区不能依赖 safety by secrecy；透明才是信任来源。他支持由不同人、用不同语言实现多个独立 kernel，让它们交叉检查，并特别提到 Mario Carneiro 的 Lean for Lean，因为它的目标是证明 kernel 正确。Collatz 事件也暴露了具体流程改进空间：Comparator 可以导出 proofs 并在 sandbox 中复查，而团队学到的一课是让 Comparator 总是下载最新版 Nanoda，这样 Nanoda 的 bug fix 能立即进入检查路径。

第三条主线，是 AI 的正面能力。Kim Morrison 用 Claude agent 做 Zlib 相关 Lean 工作：把 C 代码翻译到 Lean，修复到通过 C 版本测试套件，并证明任意压缩级别、任意数据在压缩后再解压能返回原数据。de Moura 说，这在年初看来几乎不可能。这个例子把 AI 的价值从“写高层代码”推进到“在证明约束下做底层优化”：AI 可以不断优化实现，只要不破坏已证明性质；他甚至设想，未来 AI 可以写出并证明利用处理器特殊指令的 assembly。

第四条主线，是 Mathlib 和形式化数学基础设施的规模化。de Moura 说，Mathlib 3 大约停在 110 万行，而 Mathlib 4 已约 240 万行；节目中还引用社区估计，如果要覆盖主流数学并支持任意研究级论文形式化，数学库可能需要 1 亿行。这会把 Mathlib 从“数学证明库”推向类似 Linux kernel 或 Firefox 的大型工程问题：构建系统、版本控制、多团队治理、模块边界和维护策略都会变复杂。de Moura 用 Rust crate 作类比：背景依赖齐全时，研究者只需形式化自己的贡献；如果依赖缺失，一个月的工作可能变成多年基础设施建设。

三、核心观点：推理、例子与边界

本集最重要的判断是，Lean 的可信性不来自“整个系统没有 bug”，而来自把真正需要信任的部分压缩到小 kernel，并在 AI exploit 时代继续减少必须信任的东西。Collatz 相关事件说明，风险已经从“模型生成的证明可能错”变成“模型可能构造能骗过检查器的错证明”。如果一个样本能同时利用官方 kernel 和外部 checker 的不同漏洞，绿色通过标记就不能被视为终点；检查器本身也必须接受检查。

de Moura 对这一路线划出了清楚边界：多个 checker 并不等于增加一个隐藏的验证器。他拒绝把私有 kernel 当作最后底牌，因为这会把信任从可审计机制转移到“相信某个未公开系统”。他的方案是公开多个独立实现，让不同语言、不同开发者写出的 kernel 互相制衡，并最终证明关键 kernel 正确。局限也在这里：即使 kernel 被证明正确，编译器、硬件和运行环境仍可能拉长可信链条。de Moura 自己也指出，方向只能是不断减少需要信任的东西，而不是一次性消灭所有信任。

第二个核心观点是，开源项目里的“核心”和“扩展”需要不同治理逻辑。Lean core 采用 cathedral model，不是因为社区创造力不重要，而是因为核心高度互联，随机合并会给可靠性、性能路线和长期设计带来沉没成本。相反，扩展层应该释放社区创造力。分布式协议 DSL、软件验证扩展，以及 Lean 4 暴露内部表示的设计，都是把创新放在核心之外生长的例子。这种分层的约束是，核心团队必须持续维护清晰边界；一旦边界模糊，扩展的自由就可能重新变成核心的负担。

第三个核心观点是，当前 AI 更像强大的 proof 和 implementation searcher，而不是稳定的新抽象发明者。de Moura 说，它在补证明、组合已有组件、微优化上极强，甚至在这类任务上超过人类；但一旦任务要求发明新技术或 new trick，就常常失败得很彻底。他推测这与模型训练中吸收了大量文献有关：如果问题可以由已有 trick 组合解决，模型很强；如果必须通过实验发明方法，短板就会暴露。主持人提出的“embedding space 手电筒”比喻补充了这一点：专家提供视角、种子解法和优化目标后，模型才更接近令人惊讶的表现。

这种能力边界并不削弱 AI 在形式化工程中的价值，反而解释了它为什么适合 Lean。Lean 提供强反馈：证明必须通过，性质不能被破坏。Zlib 案例展示了这种反馈如何把 AI 的耐心转化为工程价值；同样的耐心，在 Collatz 事件里也转化为安全风险。关键限制在于，proof signal 约束的是形式化目标本身；如果规格不完整、目标选错，或者检查器存在漏洞，AI 仍可能沿着错误方向高效前进。

第四个核心观点是，机器可检查 certificate 的价值不会因为模型更准确而消失。de Moura 讨论 AlphaProof、纯 LLM、Monte Carlo tree search 与神经网络路线时，没有把问题简化成哪种 AI 最终胜出；他区分的是“怎样生成 proof moves”和“是否仍需要验证”。他的回答是：即使模型正确率非常高，复杂证明仍需要 machine-checkable certificate。Boris Alexeev 在 OpenAI disproved the unit distance conjecture 后提交 120 万行 Lean 形式化证明，这个例子说明，没有人愿意逐行人工阅读这种规模的证明；形式化检查不是可选装饰，而是规模化数学和软件验证的基础设施。

第五个核心观点是，人类角色不会简单消失，而会从写每一行证明转向规格、结构和品味。de Moura 认为，AI 可以维护 boring proofs、构造新证明、降低尝试想法的成本；但关键证明仍可能由人类手写，因为它们承担美感、结构、教学和思想传播功能。Mathlib 是否收录某些内容、如何定义 ring、怎样规划数学库，也仍需要人类判断。这里的不确定性很大：de Moura 承认他无法预测五年后的状态，甚至一年前也难以预测现在的进展。因此，这不是对人类地位的永久保证，而是基于当前 AI 能力边界和形式化生态需求作出的判断。

四、学习与应用

对做可信软件、证明工具或 AI agent 基础设施的人来说，本集最直接的应用是重新画出可信边界。不要把“AI 生成了可通过检查的结果”当成终点，而要区分 kernel、库、tactic、代码生成器、外部 checker、sandbox、compiler 和运行环境。Lean 的经验表明，可信基础越小，越适合审计、交叉检查和形式化证明；但一旦从证明定理走向生成可执行程序，compiler 也会进入可信代码基，治理范围必须随之扩大。

对开源项目维护者来说，Lean 的治理经验可以转化为一个实用原则：核心层和扩展层不要使用同一种开放度。高度互联、影响全局可靠性的核心，需要明确所有权、优先级和长期设计约束；围绕核心的 DSL、工具和领域扩展，则可以让社区快速试验。取舍在于，过度开放核心会带来 bug、半成品和路线锁死；过度收紧扩展又会压制生态发现新用法的能力。

对软件团队来说，de Moura 对规格的处理尤其值得注意。规格不一定总是先以完美逻辑性质出现；一个简单、清楚、低效但正确的参考实现，也可以作为规格。团队可以先写出“要算什么”，再让 AI 优化，并要求系统证明优化后保持等价或满足性质。这适合压缩、编译器优化、数据结构替换、微优化和迁移场景；边界是，参考实现必须真的表达了想要的语义，否则 AI 只是在错误规格上跑得更快。

对采用 AI 编程的团队来说，Zlib 案例和 Collatz 事件应当一起读。AI 在有强验证信号时能做过去人类觉得烦、慢、低层的工作，比如迁移代码、修复测试、维护证明、优化实现；同样，它也可能用这种耐心寻找漏洞。实用做法不是禁止 AI，而是在关键路径上增加独立检查、版本自动更新、sandbox 复查、可审计日志和最小可信基础。尤其是内嵌 AI 的应用，de Moura 明确强调 guardrails，并希望未来能验证 guardrails 或 sandboxes；而用 AI 开发“不含 AI 的软件”相对更安全，因为主要对抗的是应用 bug，而不是运行时 AI 行为。

对数学形式化和研究工具建设者来说，Mathlib 的教训是不要只盯着单个定理。真正瓶颈常常是背景库、抽象成熟度、依赖治理和构建规模。如果缺少必要组件，形式化论文会变成基础设施工程；如果依赖齐全，研究者才可能专注于新增贡献。因此，像 Formal Frontiers 这类“人类加 AI 填补 Mathlib 缺口”的方向，价值不只是多证明几个结论，而是让更多研究级形式化任务从多年工程压缩为可执行项目。

对学习者来说，de Moura 给出的路径很务实：软件开发者可以先把 Lean 当普通编程语言用，暂时忽略证明；熟悉语法后，再证明自己代码的简单性质。AI agent 可以作为陪伴式导师，因为它读过文档、知道许多扩展，并能根据 Haskell、Lisp、C#、Java 等不同背景调整解释。这个建议的边界是：AI 很适合解释、翻译概念和引导入门，但学习者仍需要逐步建立自己对 proof moves、规格和错误边界的判断。

来源

• 原始节目：AI Can Write the Proof. Who Checks It? — Leonardo de Moura