AI 'Proves' Collatz Conjecture with Lean 4 Bug

Post

Log inSign up

Post

Gro-Tsen

@gro_tsen

So, someone came up with an AI-generated formal proof, in Lean, of a solution to the Collatz problem, and it turned out that the “proof” was merely exploiting a bug in the Lean kernel (allowing you to prove anything).

3:10 PM · Jul 29, 202656.2KViews

Gro-Tsen

@gro_tsen

3h

More details and explanations at:

infosec.exchange

abadidea (@[email protected])

Okay, we have a new contender for Most AI Thing to Ever Happen 1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem...

6.2K

Gro-Tsen

@gro_tsen

3h

Keep this in mind when someone claims that requiring formal proofs in Lean is the end-all solution to AI slop and hallucination in mathematical proofs.

6.1K

Gro-Tsen

@gro_tsen

3h

(There are other — more frequent — problems, of course, like the fact that the formally proven theorem might not match the informally understood one. Or, more basically, that the proof might be unreadable for humans, making it useless.)

5.8K

Gro-Tsen

@gro_tsen

1h

• Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem.

Jason Rute

@JasonRute

2h

Replying to @gro_tsen

I think they just use collatz as a fun way to demonstrate the lean soundness bug. There is a history of this in the theorem proving community. The author knew it was a soundness bug and it was intentional.

4.6K

Antoine Ducros

@antoineducros

3h

But doesn’t such an incident shed suspicion on plenty of Lean-checked proofs? How can one be sure that it did not already happen in a less detectable way?

3.9K

Join the conversation

Read 45 more replies