Postmortem for Kernel Soundness Bug #14576 in Lean
I report on a soundness bug in the Lean kernel that allowed an AI-assisted disproof of the Collatz conjecture. The issue involved nested inductive types and was quickly fixed, though it also exposed a separate flaw in the independent nanoda checker. This incident highlights that while metaprogramming remains essential, the kernel must strictly reject ill-typed declarations to maintain trust.
This separation and isolation of concerns is one of the main advantages of proof terms.
- gr_norm
> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both.
Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order.
- twotwotwo
This thread has some context. A proof-system researcher found some proof-system bugs and presented them a funny way:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)
The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.
- dafelst
Feels appropriate for bugs in a formal proof system:
> Beware of bugs in the above code; I have only proved it correct, not tried it.
-Knuth, 1977
- michaelfm1211
Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-...
I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system like Metamath?
- Gehinnn
Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly?
If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.