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 37.9ms across 3,260 title embeddings via pgvector HNSW
- LeanScreen: Lean Verification Hdjlaf · 30 pts · July 29, 2026 · 52% similar
- AI Meets Cryptography 2: What AI Found in OpenVM's ZkVM duha · 90 pts · July 17, 2026 · 51% similar
- Theo Conjecture solves 35-year-old math problem, finds a term no one predicted otalp · 33 pts · July 29, 2026 · 50% similar
- Are We Stuck with Lean? jjgreen · 135 pts · July 30, 2026 · 49% similar
- AI-found bugs aren't proving any easier to exploit despite the hype Tomte · 14 pts · July 29, 2026 · 49% 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...