Mastodon Feed: Post

Boosted by jonny@neuromatch.social ("jonny (nonvenomous)"):
mevenlennonbertrand@lipn.info ("Meven Lennon-Bertrand") wrote:

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 provides a sorry-free proof of the Collatz conjecture, with llm involved
- 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
- adversarial AI writing proofs 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