alt.hn

7/30/2026 at 2:26:15 PM

AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug

https://infosec.exchange/@0xabad1dea/117002106099986943

by YeGoblynQueenne

7/30/2026 at 3:36:55 PM

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

by YeGoblynQueenne