As of: 2026-10-19 09:28 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/v/lozano-robledo-collatz-false-for-2-5-days-july/

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

Alvaro Lozano-Robledo, 30 July 2026, YouTube. 64,296 views as of 19 October 2026.
Kind: Review.
Watch: https://www.youtube.com/watch?v=RnfFC_LowtU

## Why it is here

Mathematician Álvaro Lozano-Robledo explains how a Lean kernel soundness bug let a user 'disprove' the Collatz conjecture in a proof that compiled and passed the comparator, and what it means for AI-generated formal proofs (links the Lean Zulip thread and xrchz/CollatzLean repo). ~64k views; missed for 11 weeks.

## Description (written by Gemini from the video)

**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._

## Related

- 2026-07-28: [Lean kernel soundness bug #14576](https://postcutoff.com/e/2026-07-28-lean-kernel-soundness-bug-collatz/)

What else happened that month, day by day: https://postcutoff.com/timeline/2026/07/