Postmortem for Kernel Soundness Bug #14576

#1

Post by juhopitk » Sat, Aug 01, 2026, 6:32 PM UTC

Postmortem for Kernel Soundness Bug #14576
leodemoura.github.io

Re: Postmortem for Kernel Soundness Bug #14576

#2

Post by juhopitk » Sat, Aug 01, 2026, 6:32 PM UTC

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

Re: Postmortem for Kernel Soundness Bug #14576

#3

Post by vatsachak » Sat, Aug 01, 2026, 7:06 PM UTC

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.

Re: Postmortem for Kernel Soundness Bug #14576

#4

Post by de_aztec » Sat, Aug 01, 2026, 7:11 PM UTC

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

Re: Postmortem for Kernel Soundness Bug #14576

#5

Post by gr_norm » Sat, Aug 01, 2026, 7:12 PM UTC

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

Re: Postmortem for Kernel Soundness Bug #14576

#6

Post by remywang » Sat, Aug 01, 2026, 7:13 PM UTC

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

Re: Postmortem for Kernel Soundness Bug #14576

#7

Post by as1297 » Sat, Aug 01, 2026, 7:18 PM UTC

[flagged]

Re: Postmortem for Kernel Soundness Bug #14576

#8

Post by fancy_pantser » Sat, Aug 01, 2026, 7:22 PM UTC

de_aztec wrote: post #4

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

One can only trust a verifier as far as they can trust anything made out of software.

Re: Postmortem for Kernel Soundness Bug #14576

#9

Post by cperciva » Sat, Aug 01, 2026, 7:23 PM UTC

remywang wrote: post #6

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

A counterexample of the form "X cycles to X after N steps" is easy to check. A counterexample of the form "starting with X we keep going up forever" is hard to check in finite time.

Re: Postmortem for Kernel Soundness Bug #14576

#10

Post by Ar-Curunir » Sat, Aug 01, 2026, 7:24 PM UTC

as1297 wrote: post #7

[flagged]

Do you have any evidence that the bugs were due to LLM code? Or are you just speculating baselessly