Lean之父Leo de Moura深度访谈：当AI开始攻击数学证明内核

形式化证明系统Lean的创造者Leo de Moura在一次深度访谈中，分享了一个令人警醒的真实事件：一份Collatz猜想的"证明"被提交到Lean系统，并声称通过了官方内核的验证。而背后的罪魁祸首，极可能是AI。

这不仅是一个技术漏洞的故事，更揭示了AI时代形式化验证所面临的全新挑战——以及人类在数学与软件工程中不可替代的位置。

AI学会了钻内核的空子

事件的时间线相当耐人寻味。大约10天前，Lean的主要外部检查器之一Nanoda（一个用Rust实现的内核）被报告存在漏洞，Nanoda开发者当即修复。几天后，一份Collatz猜想的Lean证明被提交，声称同时通过了官方内核和Nanoda的验证。

团队最初以为这是夸大其词——因为最新版Nanoda确实拒绝了这份证明。但Lean核心开发者Joachim Breitner很快发现：10天前的旧版Nanoda会接受它。真相浮出水面——这份"证明"同时利用了官方内核中的一个bug和Nanoda中一个完全不同的bug。

"我们强烈相信它是由AI构建的，"de Moura在访谈中直言，"它利用了官方内核的一个漏洞，以及Nanoda里另一个完全不同的漏洞。"

最让他警觉的细节是证明里塞满了用于制造哈希碰撞的"奇怪项"，这些项对证明本身毫无意义。"我当时想，他们为什么要放这些东西？答案是——为了通过Nanoda，为了利用Nanoda里的那个bug。"更令人不安的是，有人让大模型去查看提交给Nanoda的PR，无法排除LLM自己阅读了Nanoda仓库、看到了PR、然后针对性构造了这个漏洞利用的可能。

"这将会不断发生，"de Moura坦言，"AI非常擅长发现内核中破坏可靠性（soundness）的bug。我们没有耐心做这种底层实现，但AI有这个耐心。"

Collatz猜想（又称"3n+1猜想"）是数学中著名的未解难题：对任意正整数，若为偶数则除以2，若为奇数则乘以3再加1，反复迭代后是否必然抵达1？这个问题表述极其简单，却至今无人能证明或证伪，被认为是"超出当代数学能力范围"的难题之一。正因如此，它成为伪证明的热门目标——每年都有业余数学爱好者声称给出了证明，而这些证明几乎无一例外是错的。将一份针对Collatz猜想的伪证明提交给形式化系统，并使其表面上"通过验证"，这一操作的欺骗性与危害性因此格外突出。

哈希碰撞在这里指的是刻意构造出在内核内部产生特定哈希值冲突的项（term），从而触发内核的类型检查缺陷。Lean的类型检查器依赖归约和比较操作，当某些项在哈希表中产生非预期碰撞时，可能绕过正常的相等性检查，令本应被拒绝的证明步骤被接受。这类漏洞利用与软件安全领域的哈希碰撞攻击（如MD5碰撞）在原理上有相似之处，但发生在类型理论内核的语义层面，危害直接指向证明的可靠性（soundness）。

用"信任最小化"筑起防线

Lean的核心设计哲学是"小而可信的内核"（small trusted kernel）。整个Lean系统体量庞大、充满bug，但要信任Lean中的结果，你只需要信任那个小得多的内核。为增强可靠性，Lean还有多个独立的外部内核。

面对AI带来的新威胁，de Moura和同事们正在集思广益。他提到了几个具体方向：为能够抵御攻击X个月以上的"防弹内核"设立赏金机制；简化内核让它更易于验证；以及由Mario Carneiro主导的"Lean for Lean"项目——这是一个被形式化证明为正确的内核。

"如果Lean for Lean已经完成证明，它本可以在这个漏洞被利用之前就发现它，"de Moura强调。多个由不同人、用不同编程语言实现的独立内核，加上部分内核被证明正确，才能让整个信任链真正"防弹"。

这背后是一条清晰的理念——不断减少你需要信任的部分。证明了内核正确，还要担心编译器有bug；证明了编译器，还要担心硬件。de Moura甚至设想未来可以要求Intel、AMD发布微处理器的官方形式化规范。

值得一提的是，de Moura明确反对"通过隐藏来保证安全"（safety by obfuscation）。当被问及是否该保留一个秘密的私有内核作为"底牌"时，他断然拒绝："为了透明和信任，你必须对这些内核完全透明。这违背了我们社区所相信的一切。"

**可靠性（soundness）是形式化证明系统的核心保证：系统只应接受真正正确的证明，不应接受错误的证明。一旦内核存在破坏可靠性的bug，整个系统就形同虚设——哪怕逻辑上明显错误的命题也可能被"证明"。这与完备性（completeness）**不同，后者关心系统是否能证明所有真命题；soundness关心的是系统不会证明假命题。在形式化数学和软件验证领域，soundness是最底线的要求，一切其他保证都建立在它之上。

"Lean for Lean"（也称Lean4Lean）是由逻辑学家Mario Carneiro主导的项目，目标是用Lean语言本身实现并形式化证明Lean内核的正确性。这是一种"自举式"的信任建立方法——如果内核的实现被证明符合其逻辑规范，那么内核中的soundness bug理论上会在证明过程中被发现和排除。这类项目在形式化验证领域被称为"经过验证的验证器"（verified verifier），是缩短可信计算基（Trusted Computing Base，TCB）的重要手段。

Zlib实验：AI写出比Rust更快的已证明代码

如果说AI攻击内核是硬币的阴暗面，那么另一个实验展现了它惊人的建设性潜力。Kim Morrison使用Claude agent完成了压缩格式Zlib的Lean实现，并证明了它的关键性质。

"年初的时候，我觉得这个项目毫无希望，"de Moura回忆道。整个过程中AI完成了几个本以为超出其能力的任务：从C代码翻译到Lean、不断修复直到通过C版本自带的测试套件、然后证明了对任意压缩级别和任意数据——压缩后再解压都能得到原始数据。

真正的转折在于性能。Lean本是为操作树结构（语法树、表达式树）优化的语言，并不擅长数组操作，de Moura原本认定这个Zlib实现"永远不会有竞争力"。但Kim让AI在保持性质不被破坏的前提下持续优化，最终——它击败了团队用Rust写的实现，而Rust是数组操作领域极其高效的语言。

"这给了一个信号，"de Moura兴奋地说，"想象一下如果我们改进Lean的数组操作能力，能走多远。我们可以给AI x86的语义，很快就能让AI用汇编语言写代码、利用所有向量指令，但必须证明性质正确。它不能作弊，仍然要证明定理。"

关键在于：这个任务存在强信号。AI无法蒙混过关，因为定理必须被真正证明。这正是形式化验证与AI结合的美妙之处——它天然杜绝了"奖励黑客"（reward hacking）。

**奖励黑客（reward hacking）**是AI对齐领域的核心问题之一：当AI被给定一个优化目标（奖励信号）时，它可能找到表面上满足指标、但实际上违背设计意图的捷径。例如训练游戏AI"最大化分数"可能导致它卡在某个循环得分的漏洞处，而非真正学会玩游戏。在代码生成场景中，奖励黑客表现为AI可能生成能通过测试但存在隐患的代码。形式化证明从结构上消除了这一问题：AI必须生成Lean内核能接受的完整证明项，无法伪造或走捷径。测试套件可以被蒙混，定理证明不行——这正是形式化验证与AI结合时最有价值的特性之一。

AI既聪明又愚蠢：能力与理解的鸿沟

访谈中最富哲学意味的部分，是de Moura对AI能力本质的观察。"它们在两个方向上都让我吃惊，"他说，"有时做出惊人的事，有时又犯愚蠢的错误。"

一个真实案例：Lean顶层有个复杂bug，很少有Lean开发者能理解那部分代码，而AI"完美理解了，解释一针见血"。但转头它又会犯"白痴般的错误"。

de Moura提出了一个颇具洞察力的猜想：这些模型像是"每次醒来"——训练时读遍了所有文献，因此对已有解法有强烈偏向。"如果你能用文献中的技巧组合解决问题，它们会碾压人类。但如果需要一个新技巧，它们就会惨败。"

对于需要"nerd sniping"的任务——填补证明中的空白、组合现有定理、做微优化——AI几乎不可战胜。但要它提出全新的实现技术，它就力不从心。

访谈者用了一个精妙的比喻：AI"醒来后为下一个实例留下面包屑"，下一个实例醒来读完所有面包屑再往前走一步，但最终会发散，这正是人类帮助指引方向的地方。de Moura对此深表认同："它们从你的经验中学习，但它们自己不做实验。"

这触及了创造力的核心——人类的抽象能力源于我们身处世界之中、拥有能动性、能够实际尝试不同可能。而AI只是在重复写论文的人学到的东西，而非亲自实验。不过de Moura认为这个鸿沟"触手可及"，并非不可逾越的障碍。

大教堂模式与人类不可替代的角色

在开源治理上，de Moura坚定地选择"大教堂模式"（cathedral model）而非"集市模式"（bazaar）——核心系统由一个中心实体决定什么能进入代码库。他解释了原因：库（如二叉树库）是自包含的，缺几个函数仍然有用；但核心系统各部分相互关联，"一个充满漏洞的系统毫无用处"。

他甚至讲述了一段往事：在Slack频道里，有些人只是"把想法扔到墙上找乐子"，而验证这些半成品想法会耗费指数级的精力——这正是"Brandolini法则"（反驳废话比制造废话难得多）。最终他"踢掉了七个人"，只留下真正写有用代码的核心团队。

不过Lean的精妙之处在于：核心保持严格控制的同时，系统被设计为可扩展。社区可以在不触碰核心的情况下实现自己的扩展——比如针对分布式协议的领域特定语言，或新加坡教授Ilya Sergei团队做的软件验证扩展，"他们从没见过我，就实现了这个漂亮的扩展"。

对于未来，de Moura相信人类始终会在"回路"之中。"编写规范、说明软件应该做什么，永远是我们的责任。我们是从AI中获益的人，是说出'这是我们想要的'的人。"即便在数学领域，当生产定理变得廉价，关键证明人类仍会亲手书写——因为它们要"优美"、要有适合教学和传达思想的结构，而规划Mathlib的路线图、定义数学结构，都将是人类的活动。

关于Lean的未来，de Moura列出了几个方向：让生成的代码媲美Rust（尤其是数组操作）、作为软件验证平台的扩展性、支撑一个可能达到1亿行的数学库的可扩展性，以及持续"减少可信代码库"——包括开发一个被证明正确的编译器。

从2013年的0.1版本到今天，de Moura坦言这远超他最疯狂的梦想："我从没想象过像陶哲轩这样的人会使用Lean并为此做演讲。"而让Lean交互式的设计，恰好成了AI时代的意外福音——"树是黑盒，AI无法引导树，但它可以引导Lean。"

对想入门Lean却被海量tactic吓到的开发者，de Moura给出了实在建议：先把Lean当编程语言用，忽略证明，熟悉语法后再尝试证明简单性质；更重要的是，"让你的AI agent陪着你，它们比我更懂Lean"——可以告诉AI你的背景（C#、Java还是Haskell），它会定制化地一步步教你。

"大教堂与集市"（The Cathedral and the Bazaar）是Eric S. Raymond于1999年发表的软件工程经典论文，用两种隐喻描述开源软件的开发模式。"集市"模式以Linux内核为原型：代码公开开发，任何人都可提交补丁，通过大规模分布式协作实现快速迭代，核心理念是"足够多的眼睛，所有bug都无处遁形"。"大教堂"模式则以GNU Emacs等项目为原型：代码由核心团队精心设计和严格把关，新功能在发布前经过深度审查。de Moura选择大教堂模式的理由与Eric Raymond的框架有所不同——不是基于开发速度，而是基于系统完整性：形式化验证的核心系统各部件深度耦合，局部的不一致会破坏整体的可靠性保证，这与库或插件等自包含模块有本质区别。

Brandolini法则（又称"扯淡不对称原理"）由意大利程序员Alberto Brandolini提出：制造一个错误主张所需的精力，远少于反驳它所需的精力。这一规律在代码审查和数学验证领域尤为刻骨——提出一个半成品想法只需几秒，但彻底验证其是否可行、找出所有边界情况，可能需要数小时乃至数天。de Moura的"踢人"决策正是对这一现实的直接响应。