The Collatz Conjecture was FALSE (for 2.5 days in July)

Overview

The video reports a short-lived “break” in trust surrounding a formal proof in the Lean theorem prover: a purported disproof of the Collatz conjecture (“3x + 1”) was verified as false for about 2.5 days in late July, before the underlying problem was fixed.

What happened

On July 25, a GitHub user, Romano Kumar, posted a Lean/Mathlib package that:

• formalized the Collatz conjecture in Lean,
• stated a theorem claiming the conjecture is false (by exhibiting an orbit that does not return to 1),
• included Lean-based verification intended to show the package was correct.

Why it was believed briefly

The proof was briefly accepted because:

• it was accepted by Lean’s system, and
• it was additionally checked by a tool (“comparator”) designed to ensure the proof matched the theorem being claimed—i.e., not cheating by relying on mismatched claims or dubious external axioms.

The core issue

Shortly afterward, developers identified a bug in the Lean 4 kernel that the false proof exploited.

The video describes the vulnerability as involving:

• nested inductive types, and
• how the kernel could accept “ill parameters,” allowing an invalid argument to be treated as a valid proof.

Timeline and fix

• By July 28, around 1:00 a.m., a patch was submitted to correct the kernel bug.
• After the patch, the erroneous proof no longer represented a genuine disproof.

Community reaction

The episode triggered concern across the Lean community because the bug appears to have been present in multiple stable versions for a long time.

The video also suggests:

• the bug may have been uncovered through AI/LLM-driven vulnerability hunting, and
• broader fears that other kernel vulnerabilities could exist and potentially allow additional incorrect proofs to pass verification.

Closing stance

Despite the panic, the speaker emphasizes:

• respect for the Lean community, and
• that Lean is maintained by volunteers,
• with an expectation that additional security checks and safeguards will be introduced after incidents like this.

Presenters / Contributors

• Romano Kumar — the GitHub user who posted the initial Lean package claiming the disproof.
• Video speaker/presenter — not named in the subtitles.