EDIT: I jumped too fast on the easy story, and overplayed the role of AI here. Had I known how it would blow up, I would have been more careful... Things are still not entirely clear, but I've tried to make the post less wrong.
---------------------
This whole Lean kernel bug is almost too on point to be true, it fits perfectly in the discussions we've had here and elsewhere over the last months/years…
To summarize:
- formal methods researcher (@ramana) sets up a repo with a sorry-free proof of the Collatz conjecture
- the proof is reporting (by @kirancodes) as being a kernel bug, the repo was a tongue-in-cheek way of exposing the bug
- Ramana mentions llms were
involved (but how is unclear atm)
- the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel's code is the reference
- external checkers (lean4lean and nanoda from a week ago) are affected too, either because they copy the reference kernel implementation, or because (nanoda) of a missing check in this subtle part of the code
- the bugs compound, and the invalid proof is accepted by comparator, Lean's gold standard for proof checking
And so
- adversarial AI writing proofs raises the bar for kernel correctness
- without a clear type-theoretic understanding of what is actually implemented, we're toast
- external checkers help to catch implementation bugs, but without a clear specification they can't really catch logic bugs
I believe the whole story also showcase the solidity of human measures: the bug was fixed as soon as found, with healthy discussions between experts, in the open, as to what to do. At no point was there any real doubt as to the solidity of a mechanised result.
Meven Lennon-Bertrand
@mevenlennonbertrand@lipn.info
