2026年8月1日，在7月27日的那一周，Lean内核中的一个健全性错误（#14576）被报告并修复。该问题在Zulip和社交媒体（例如，X、LinkedIn和Mastodon）上得到了关注。发生了什么事情 7月25日，Ramana Kumar发布了一个包含无错误的Collatz猜想“反证”的仓库，该反证是通过AI协助创建的。它不是有效的证明，因为它利用了内核处理嵌套归纳类型的一个错误。7月28日，Kiran Gopinathan将其简化为一个小的错误证明，并打开了问题#14576。我们在报告后一个小时内推送了修复（#14577）。Joachim Breitner对其进行了评审并提出了改进建议，然后它被合并。新的补丁版本已发布。错误：当内核在具有参数Ds的归纳类型T下消除嵌套出现时，这些参数是幻像的（未在构造函数字段中提及），它们会从生成的辅助类型中消失，从而逃避类型检查。在该位置的一个错误类型参数可以使内核接受一个错误的证明。该错误只能通过元编程到达，直接将归纳声明发送给内核。前端检查参数并捕获错误类型的项。这是一个实现错误，而不是Lean元理论中的漏洞。为什么nanoda未能捕获它 原始的Collatz仓库也通过了一个星期前的nanoda版本，即主要的外部检查器。nanoda是一个独立的内核（即证明/类型检查器），由Chris Bailey用Rust实现。令人惊讶的是，涉及两个不相关的错误。官方内核在嵌套归纳类型支持中缺少检查，如上所述。nanoda确实检查了那个点，但没有验证投影节点中的类型名称。nanoda的错误由Jeremy Chen报告，并在Lean错误报告前一周修复。证明是构建的，以便内核永远不会检查的表达式是旧的nanoda所接受的。Ramana认为时机是巧合，但无法排除模型见过nanoda报告的可能性。Joachim提出了一个假设，即时间巧合是由于能够找到此错误的强大模型的可用性。实际后果：与独立内核的检查仍然有效，因为它需要两个实现中的两个不同错误，但依赖于它的用户需要这两个的当前版本。lean4lean受到内核错误的影响，因为它对归纳形式的处理是参考实现的移植。验证 Mario Carneiro的lean4lean是一种对Lean类型理论的正式化，连同证明内核能够实现它。该工作仍在进行中，健全性证明尚未涵盖归纳类型，而待验证的实现遭受了与官方内核相同的错误。该错误将在尝试结束该部分的验证时被发现。关于移除元编程 讨论中有一个建议是移除或限制元编程，以便此攻击不可表达。这是错误的。该扩展程序是设计上不可信的。健全性不能依赖于一个不可信的组件拒绝构建一个坏项。想要提交恶意证明的攻击者也可以直接编写.olean文件或修改内存，这两者都完全绕过了扩展程序。内核必须自己拒绝错误类型的声明，在其自己的过程中。这种关注的分离和隔离是证明项的主要优点之一。FRO正在做的事情 针对该漏洞的回归测试，以及Arthur Adjedj提出的相关非均匀参数案例，正在内核竞技场中进行。后续的PR（#14582）使内核检查嵌套出现的参数是否确实表现为参数，而不仅仅是重新类型检查它们。OpenAI的Daniel Selsam协助Lean FRO使用专门用于网络安全的AI，并发现了Lean内核中的其他编程错误。这些错误都已修复。所有这些错误都是通过元编程到达的。PRs：#14607、#14608、#14609、#14613、#14615、#14616。我们还加强了内核不变式。PRs：#14621、#14631、#14632。comparator.live现在默认运行nanoda，且nanoda每天获得跟踪，以便在上游修复后，lean-eval和comparator保持最新。我们正在联系并支持可以发现进一步错误、开发新内核以及在理论或经过验证的内核上工作的专家。致谢 我感谢Joachim Breitner和Sebastian Ullrich对这一帖子提出的修订和建议。