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:
1 comment
[ 243 ms ] story [ 222 ms ] threadhttps://leanprover.zulipchat.com/#narrow/channel/270676-lean...