A False “Refutation” of the Collatz Conjecture Exposed a Bug in Lean's Kernel

Leonardo de Moura, co-founder and chief architect of Lean FRO, has published a postmortem on a soundness bug in the kernel of the Lean interactive proof system. The story turned out to be instructive: the weak spot was found not by hand, but with the help of artificial intelligence.

What happened

On July 25, Ramana Kumar posted a repository containing a formally “clean” (no sorry) refutation of the Collatz conjecture, constructed with the participation of AI. Of course, no one had actually refuted the conjecture: the “proof” exploited a bug in the handling of nested inductive types. A few days later, Kiran Gopinathan reduced it to a short derivation of False and filed issue #14576. The fix was shipped an hour after the bug was reported.

The essence of the defect: when the parameters of a nested inductive type turn out to be “phantom” (not mentioned in the constructor fields), they disappear from the auxiliary type and drop out of the check. By slipping an ill-typed argument into that position, one could make the kernel accept a proof of False.

A subtlety with the independent checker

The most curious part is why the forgery wasn't caught by nanoda, an independent implementation of the Lean kernel in Rust. It turned out that two unrelated bugs in two different checkers were involved at once. The official kernel failed to check one place, and nanoda another (the type name in a projection node). The “proof” was arranged so that the expression the kernel doesn't look at at all happened to pass the old version of nanoda. The nanoda bug, tellingly, had been fixed a week earlier. Kumar considers the coincidence accidental, but doesn't rule out that the model had seen the nanoda bug report.

De Moura's practical takeaway: cross-checking with an independent kernel still works — deceiving it required two separate errors in two implementations — but you need to use up-to-date versions of both.

On metaprogramming

In the discussion, there was a suggestion to remove or restrict metaprogramming so that such an attack couldn't even be expressed. De Moura calls this a misconception: the elaborator is by definition not a trusted component. Soundness cannot rest on an untrusted part refusing to assemble a bad term — an attacker can already write .olean files directly or edit memory. Rejecting incorrect declarations is the job of the kernel itself, in its own process.

What's next

Regression tests have been added, and a separate PR now checks that the parameters of a nested occurrence really do behave as parameters. Daniel Selsam of OpenAI helped Lean FRO with a cybersecurity-specialized AI and found several more software bugs in the kernel — all fixed, and all, incidentally, caught by nanoda. The comparator.live tool now runs nanoda by default and tracks it daily.

Source: Hacker News