Lean publishes a postmortem for kernel soundness bug 14576 after an AI-assisted false disproof of Collatz passed both the official kernel and a then-week-old version of the main external checker

Sources: postmortem, HN discussion
Summary: Leonardo de Moura published a first-party postmortem for Lean kernel soundness bug 14576. The post states the bug was reachable only through metaprogramming, that lean4lean is affected by it, and that the fix landed about an hour after the report. The Collatz repository also passed a week-old version of the external checker nanoda, and the postmortem states that the nanoda bug was reported by Jeremy Chen and fixed a week before the Lean bug was reported, so the false disproof required two distinct bugs in two implementations. The post also records that an OpenAI cybersecurity model run by Daniel Selsam found further kernel mistakes, all of them caught by nanoda.
Why it matters: The postmortem concludes that checking with an independent kernel still works, so anyone treating a Lean certificate as verification needs current versions of both the kernel and the external checker rather than whichever build was to hand.