alt.hn

7/29/2026 at 6:50:47 PM

AI "Proves" Collatz Conjecture with Lean 4 Bug

https://twitter.com/gro_tsen/status/2082483878480977959

by pfdietz

7/29/2026 at 7:20:51 PM

At least 3 times a week, someone on the r/Collatz sub-reddit says: "I came up with a proof for Collatz and had ChatGPT/Claude verify it and it thinks I'm a genius."

It's so common, the community barely comments on the absurdity of these posts any more.

by jones1618

7/29/2026 at 7:59:20 PM

This was a bit different, in that Lean was involved. That's more concerning.

(I'm told this actually wasn't found by looking for a proof for Collatz, just that Collatz was used to exhibit the bug, once found.)

by pfdietz

7/29/2026 at 7:47:50 PM

Maybe someday AI will find a bug in the code for the simulation of this universe and use it to solve whatever prompt the user put in front of it, so be careful what you wish for.

by hyperhello

7/29/2026 at 8:06:12 PM

…minutes before a bunch of Vogons show up to finally get started with their intergalactic highway and the result never makes it to the prompter ;)

by btschaegg