Meven Lennon-Bertrand on Nostr: This whole Lean kernel bug is almost too on point to be true, it fits perfectly in ...

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:
- an AI agent let loose provides a sorry-free proof of the Collatz conjecture
- the proof is detected as actually being a kernel bug
- 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) reproduce the bug, because they essentially copied the reference kernel implementation

And so
- AI raises the bar for kernel correctness by a lot
- 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 catch logic bugs