AI能写出证明，谁来检查？——Leonardo de Moura
摘要
Lean的战略优势，在于一个治理严格的核心，外围则是无需许可的扩展层。 Leonardo de Moura反对随机堆积 pull request，因为漏洞、未完成的功能和过早的设计承诺，可能束缚整个系统。Lean FRO如今由20人共同负责维护，将这项守护责任分散开来；而可扩展性则让外部开发者无需触碰可信核心，就能构建出令人意外的领域专用工具。
一次看似推翻Collatz猜想的证明，暴露了AI正在改变攻击证明检查器的经济学。 据称，这份提交同时利用了Lean官方内核中的1个漏洞，以及Rust实现的Nanoda检查器中的另一个无关漏洞；de Moura表示，他们确信这是AI生成的。Joachim的调查提出，某个LLM可能看过另一个代码仓库中的 pull request，随后拼出了这套攻击。结论在操作层面十分紧迫：“AI非常擅长发现逻辑错误和内核漏洞。”
Kim Morrison借助AI开发的zlib项目，让形式化验证的底层软件从近乎不可行变得开始可行。 Claude Code代理将C代码翻译成Lean，实现了与C测试套件的兼容，证明对任意压缩级别和输入，压缩后再解压都能得到原始数据，随后又将大量使用数组的实现优化到接近Rust的方案。Scarfe说：“我们没有耐心做这种底层实现，但AI有。”
AI可能让规范驱动开发成为日常，但无法免除决定软件应该做什么的艰苦工作。 规范来自用户反馈，会在部署后继续变化，并可能使生成的代码及其证明失效；AI的价值在于更新这些产物，让验证能够经受迭代。一份简单、未优化的Lean实现本身就可以充当规范，供AI据此推导出等价的优化版本。
Mathlib正面临AI放大的规模扩张问题，而不是定理产出不足。 Lean 4的库已经达到240万行，Lean 3则为110万行；de Moura引用的估计认为，要覆盖任意科学论文，代码规模可能需要达到1亿行。尽管Mathlib从2025年至今增长了44%，编译时间却下降了10%，AI仍可能让库的增长速度超过人类在性能优化和治理上的处理能力。
当前模型擅长有边界的“狙击式证明”，但在抽象、实验和选择正确方向上仍不可靠。 它们可以填补证明缺口、解释晦涩的内部机制，并在微观代码优化上胜过大多数人类，却仍会犯“愚蠢的错误”，而且往往是在复现既有技巧，而不是发明新方法。人类持久的角色在于品味：确定方向、组织库、选择值得解决的问题，并保留具备解释力的证明。
即便模型原始准确率接近99.99999%，机器可验证的证书仍不可或缺。 Boris Alekseev围绕单位距离猜想写下的120万行Lean证明，说明了为什么“没人想逐行检查这样的证明”。无论证明来自GPT-5.6、Claude Fable、蒙特卡洛树搜索还是未来的系统，Lean的机会都在于检查每一步，并逐步验证内核、编译器以及外围的信任链。
精读
1. Lean的核心像大教堂，生态因此可以像市集一样运转
Tim Scarfe借Quake 3速通来描述这种张力：社区往往会把非预期行为转化为创造性文化。de Moura的回答是，他如今已不再亲自控制Lean的核心；Lean FRO大约有20人，每名开发者负责一部分组件，并决定是否接受外部 pull request。
不过，de Moura仍然“坚定相信核心开发应采用大教堂模式”。库即便不完整，仍可能有用；但一个高度互联、内部“漏洞百出”的核心则无法正常运转。随机贡献会引入漏洞、半成品功能和设计承诺，最终阻碍更重要的优化。
他的平衡手段是可扩展性。社区成员可以为分布式协议、命令式软件验证等领域创建专用语言，而无需修改Lean核心。有次演示让他惊讶到一开始坚持说：“这不是Lean。”后来他才发现，那完全是一个Lean扩展。
2. 廉价的想法生成，制造昂贵的治理问题
de Moura回忆说，他曾把一些人踢出Zulip频道，因为他们不断提出想法，却从不把想法做出来。每一次浮于表面的修改，都会让下一个缺陷更难暴露：“在一个未完成的想法里找漏洞，所需时间会以指数级增长。”
Scarfe将这段经历与Brandolini定律和生成式AI联系起来：提出看似合理的建议成本很低，反驳它们却要消耗专家注意力。de Moura抱怨的并不是创造力本身，而是责任不对称——一边把头脑风暴当作消遣，另一边却要由核心团队把系统真正做出来。
Lean FRO已经实质性地改变了这种负担。当一个严重的内核问题出现时，Joachim Breitner负责技术调查、向社区解释以及协调工作；de Moura说，以前把工程处理和公开沟通结合起来，“对我来说会是一场噩梦”。
3. Collatz漏洞利用让证明检查变成AI安全问题
事件发生前大约1周或10天，Nanoda刚发现并修复了一个漏洞。Nanoda是Lean主要的外部内核之一，以Rust实现。随后出现了一份声称推翻Collatz猜想的证明，据称它同时通过了官方Lean内核和此前存在漏洞的Nanoda实现。
调查发现了2个彼此独立的漏洞利用：其中一个针对Lean官方内核，已被de Moura修复；另一个则利用看似无关的哈希碰撞机制，攻击Nanoda中的不同缺陷。即便两者的重合可以被解释为巧合，也不能排除某个LLM看过另一个代码仓库中的 pull request，随后构造出这套组合攻击。
眼下的防御措施既普通又关键：Lean的比较器负责导出证明，并在沙箱中测试这些证明，因此应该始终拉取最新版本的Nanoda，而不是等待手动更新。更长期的方案是增加由不同团队独立实现的内核，并支持Mario Carneiro的Lean4Lean工作。Lean4Lean已经证明了许多部分，但尚未完成全部证明；它最终的价值，在于得到一个已被证明正确的内核。
Scarfe提出，可以设置一个私有、隐藏的内核，就像私有的基准测试集。de Moura拒绝了这个前提：“我不喜欢通过混淆或隐藏来实现安全。”信任应当来自透明的实现、多样性和正确性证明，而不是一个无法验证、却被当作最终裁决的秘密检查器。
4. AI让经过验证的底层优化开始变得可行
de Moura最初认为Kim Morrison的zlib项目“毫无希望”。但Claude Code代理还是把C实现翻译成Lean，不断修复直到通过C测试套件，并证明对任何输入、任何压缩级别，先压缩再解压都会返回原始数据。
正确性得到证明之后，真正的意外才出现。Lean针对语法和表达式树做了优化，而不是针对数组；但在AI持续引导下优化后，代码变成了某种接近Rust方案的实现，同时保留了原有证明。de Moura更新后的判断很直接：“去年我认为这是不可能的，但现在它相当可行。”
他的进一步推演是经过验证的汇编：向AI提供形式化的x86语义和一个汇编器，让它利用复杂指令，同时证明所需性质。Scarfe说，人类没有耐心做这种底层工作；de Moura则指出，每个证明义务都会清晰反馈优化是否仍然有效。
5. 规范越不完整，反而越有价值
Scarfe的质疑是，真实软件很少从一份稳定规范开始；团队正是因为在迭代中不断发现需求，才会采用敏捷开发。de Moura对此表示认同：用户会持续要求更多控制、更少行为、另一个复选框，或把证明放到不同位置，因此规范是“一场持续的对话”。
他的实际做法，是把一份未优化的高层Lean程序当作可执行规范：先不使用复杂算法，实现“最简单且正确的想法”，然后让AI生成更快的实现并证明二者等价。这样既能捕捉已知行为，也不会假装所有需求都已经确定。
规范一旦改变，代码及其一致性证明就会失效；在过去，这会让形式化验证变得极其昂贵。de Moura预计AI可以同时更新二者，但过渡期内会出现一种抱怨：每次规范变化，都可能需要“数十亿个token来更新所有东西”。
终点似乎是把验证嵌入日常开发。工程师只需编写性质并提交 pull request，系统则在界面背后检查代码变更是否保留这些性质，即便用户并没有意识到自己参与的是形式化验证。
6. Lean 4的可扩展性为AI做好准备，Mathlib则进入工业级规模
Lean 0.1是de Moura制作的一个小巧、但几乎无法使用的依赖类型理论训练工具；Lean 2的用户规模可能只有50-100人。Adam Chlipala要求策略可由用户扩展，这一需求塑造了Lean 3；此后Mathlib快速增长，也暴露出只扩展策略、却不扩展整个系统的局限。
Lean 4完全用Lean重建，从2018年初一直到2020年末才实现自编译。它的内部表示可以从普通Lean文件中访问：研究人员能够提取证明数据，开发者也可以构建复杂的验证语言，而不必修改平台本身。
依赖类型提供了统一机制：一个包含整数X和Y的结构，可以要求第3个字段证明X大于Y；一个函数也可以要求传入值Y不为0的证据。前置条件、后置条件和不变量，都可以被建模为类型。
Mathlib 4已有240万行，Mathlib 3则为110万行；一些社区估计认为，要完整覆盖科学领域，规模可能接近1亿行。它的统一抽象很有价值——“只有一个环”——但这样的规模可能需要由不同维护者负责的一组协同库，而不是一个单一的巨型库。
7. AI可以生成证明，但人类仍要决定哪些数学值得保留
de Moura看到模型在做两件看似互相矛盾的事：它们可以完美解释晦涩的内部机制，却在顶层的简单问题上犯错。模型擅长“狙击式证明”——填补一个明确的缺口、组合已知引理，或微调代码性能——但“如果你让它们想出一种全新的做法，它们会惨败”。
Scarfe把专家提示比作一束射向嵌入空间的手电筒：人类提供有希望的方向、初始构造、有用技巧和精确目标。模型可以沿着光束出色推进，但它们的记忆仍然只是“留给下一个人的碎片”，而不是对理解进行持久重组。
de Moura认同，要求LLM实现SMT时，它往往是在重复教材，而不是开展实验。通过实践学习，并根据经验更新权重，可能提供缺失的视角；但持续自我适应的代理社会也会让安全和问责变得更加复杂。
无论最终胜出的是哪种生成器，验证都不会消失。120万行的形式化证明不可能由人类手工审计；即便模型准确率达到99.99999%，仍然需要证书。尚未解决的竞争在于经济性：混合搜索可以执行大量廉价步骤，而GPT-5.6或Claude Fable执行的步骤更少、成本更高。
因此，Lean的路线图是把信任逐层向下推进：达到可与Rust竞争的数组性能，验证整个系统，处理可能达到1亿行的库，并构建经过验证的编译器，让可执行软件不再依赖对实现的信任。路线图仍由人类掌握——规范、抽象、库的准入机制，以及足够优美、能够传授知识的关键证明。