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

Summary
Mathematician Álvaro Lozano-Robledo discusses an incident from late July 2026 where a bogus disproof of the Collatz Conjecture was accepted and verified as true by the Lean 4 interactive theorem prover. He explains that the proof was an exploit of a kernel soundness bug discovered with the aid of LLMs, which was patched within 2.5 days after an issue and minimal proof of “False” were reported.

What is shown

• [00:00] Álvaro Lozano-Robledo opening with a Collatz tree diagram and graphic stating “The Collatz Conjecture was False for 2.5 days in July”.
• [00:28] A post on X by Elliot Glazer referencing Ramana Kumar’s Lean refutation of Collatz checked by Comparator.
• [00:34] Explanation slide detailing Lean’s sandboxed proof verification tool (comparator) and checker functions.
• [00:50] Timeline post by Jack McCarthy detailing Ramana Kumar’s July 25, 2026 commit disproving the Collatz conjecture and noting the involvement of an LLM.
• [00:59] Code snippets from the GitHub repository (Collatz/Main.lean), showing theorems claiming non-terminating orbits.
• [01:19] Verification pipeline screen showing flags, leanchecker, and checking with Nanoda.
• [01:29] Lean 4 issue #14576 opened by Kiran with an MWE “Proof of False”, followed by Leonardo de Moura’s fix (PR #14577).
• [01:45] Leonardo de Moura’s GitHub commit description: “fix: missing check at kernel inductive declaration”.
• [01:59] List compiled by Martin Dvořák of 24 stable Lean 4 versions (4.22.0 through 4.32.1) where the bug could be reproduced.
• [02:41] Community forum posts questioning how such a kernel bug remained undetected for multiple versions.
• [03:06] The official Lean website (lean-lang.org) as the presenter commends the Lean developer community.

Claims & numbers

• The Collatz conjecture was formally verified “false” in Lean for approximately 2.5 days in July 2026 (the presenter states).
• The proof commit was submitted by Ramana Kumar on Saturday, July 25, 2026, at 4:12 PM (shown on screen).
• Lean 4 issue #14576 (“Proof of False”) was filed on Monday, July 27, 2026, at 11:28 PM, and Leonardo de Moura issued fix PR #14577 on July 28 at 1:08 AM (shown on screen).
• The presenter states the bug stemmed from nested inductive datatypes where parametric arguments escaped type checking.
• A list shown indicates the bug was reproducible across Lean 4 versions from 4.22.0 through 4.32.1.
• The presenter notes reports indicating the vulnerability was uncovered using an LLM / AI tool.

Notable quotes

• [00:00] “Breaking news: the Collatz conjecture, the 3x+1 problem, was false—verified false, like formally verified false using Lean—for 2.5 days in July.”
• [00:16] “...until they fixed the bug in the kernel in Lean that this proof was exploiting, which of course was not a proof, it was just an exploit of a bug.”
• [03:06] “The Lean community has all my respect. This is an incredibly important project, especially in this era of math and AI, and it is built by a community of volunteers.”

Assessment
This is an authentic informational review and commentary by a mathematician analyzing a documented GitHub vulnerability and commit timeline. The screenshots and code shown reflect real Lean repository commits, issues, and community discussions.

Described by gemini-3.8-flash on 2026-10-19 from the video’s audio and frames.