3 ms·
AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug
- YeGoblynQueenne 3mo agoThe 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-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613480044 https://leanprover.zulipchat.com/#narrow/channel/270676-lean...