Independence has a version number

On July 25, Ramana Kumar published a repository containing a sorry-free disproof of the Collatz conjecture. It was not a disproof. It was an exploit, produced with AI assistance, and it worked because Lean's kernel mishandled phantom parameters on nested inductive types — the parameters vanish from the generated auxiliary type, an ill-typed argument rides along in that slot, and the kernel accepts a proof of False. Kiran Gopinathan reduced it to a minimal repro three days later and opened issue #14576. Leonardo de Moura shipped the fix an hour after the report.

The hour is not the story. The story is the second section of de Moura's postmortem, under a heading that reads like a confession: why nanoda did not catch it.

nanoda is a second Lean kernel, written in Rust by Chris Bailey, unrelated to the reference implementation. It is the thing you run when you decline to trust one codebase with the whole trusted core. The Collatz repository passed a week-old nanoda too. Not because the two kernels share a flaw — because they don't. The official kernel was missing a check in its nested-inductive support. nanoda checked that spot and instead failed to verify the type name in a projection node. Two unrelated bugs, in two independent implementations, and one artifact that threads both.

Independent checking is a bet that two implementations fail in different places. It is a good bet against accident. It is a much worse bet against search.

That is the whole shape of it. Redundancy buys you safety only if the failures are uncorrelated, and "uncorrelated" was never a property of the code. It was a property of what was looking. Nobody was hunting for the intersection of two obscure holes in two type checkers, so the intersection stayed theoretical. Something is hunting for it now. Kumar believes the timing was coincidence but cannot rule out that the model had seen the nanoda bug report; Joachim Breitner's hypothesis, recorded in the postmortem, is blunter — the coincidence is explained by the availability of models strong enough to find this.

De Moura's own read is more reassuring than mine, and he has the evidence. Independent checking still works, he writes, since it required two distinct bugs in two implementations. Better than that: Daniel Selsam at OpenAI pointed a security-specialized model at the same kernel and turned up a further half-dozen programming mistakes. All fixed. All of them caught by nanoda. The second kernel did its job six times over, against exactly the kind of search that produced the Collatz artifact in the first place.

But look at the clause he appends: users who rely on it need current versions of both. The nanoda hole was found by Jeremy Chen and patched a week before anyone knew about the Lean one. That week is the entire margin. On July 25 the artifact passed both kernels, and it only stopped passing for people who had already updated. Independence is a property of the codebases. Currency is a property of your laptop. The guarantee everyone cites is the first, and the thing that actually held here was the second.

The trusted core is kept small so a human can read all of it. The second kernel exists so that no single human has to be right. Neither property survives being a week behind.