AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug
YeGoblynQueenne
14 points
1 comment
July 30, 2026
Related Discussions
Found 5 related stories in 298.6ms across 6,607 title embeddings via pgvector HNSW
- Fermat's Last Theorem in Lean 4 aaraujo002 · 83 pts · September 04, 2026 · 54% similar
- OpenAI Says It Has Cracked One of Math's 'Millennium Problems' doener · 13 pts · September 08, 2026 · 52% similar
- LeanScreen: Lean Verification Hdjlaf · 30 pts · July 29, 2026 · 52% similar
- OpenAI’s Navier-Stokes release included a Lean 4 formal proof ibobev · 153 pts · September 10, 2026 · 52% similar
- OpenAI might have stolen another major proof tamnd · 59 pts · September 10, 2026 · 52% similar
Discussion Highlights (1 comments)
YeGoblynQueenne
The plot thickens! It seems the researcher who posted the "proof" of the Collatz conjecture was aware of the Lean bug; or maybe he wasn't. He's currently being coy about it and it's hard to say if he's trying to save face or genuinely intended to cause a stir for whatever reason: https://leanprover.zulipchat.com/#narrow/channel/270676-lean...