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 156.1ms across 10,991 title embeddings via pgvector HNSW
- What mathematicians should know about the Lean Theorem Prover: reliability & AI matt_d · 76 pts · October 09, 2026 · 57% similar
- Fermat's Last Theorem in Lean 4 aaraujo002 · 83 pts · September 04, 2026 · 54% similar
- AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura datascientist · 11 pts · October 29, 2026 · 53% 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
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...