Postmortem for Kernel Soundness Bug #14576

> 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.

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

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.

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?

And everyone who's been into this stuff for a while has had their prediction come through.

If AI is water, Lean is the pipe and collatz is a clog on one end, then surely we'll find the cracks.

Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?

So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.

"A soundness bug in the Lean kernel (#14576) was reported and fixed during the week of July 27. [...] On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576."

Lean has Claude contributions, what do you expect!

Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.