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 421.5ms across 15,510 title embeddings via pgvector HNSW
- Leanstral 1.5: Proof abundance for all programLyrique · 159 pts · July 03, 2026 · 55% similar
- Lean proved this program correct; then I found a bug bumbledraven · 184 pts · April 14, 2026 · 53% similar
- LeanScreen: Lean Verification Hdjlaf · 30 pts · July 29, 2026 · 52% similar
- The New Linux Kernel AI Bot Uncovering Bugs Is a Local LLM on Framework Desktop guerby · 12 pts · April 26, 2026 · 51% similar
- Lf-lean: The frontier of verified software engineering alpaylan · 18 pts · March 12, 2026 · 51% 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...