Alleged Collatz Conjecture proof

Stream: general

[Alex Sweeney]

I saw someone claim they've proved the Collatz Conjecture in Lean 4 with no sorry. I'm not experienced enough to check it, but it looks like a pretty short proof. I'm skeptical but would love if this was real.

[Alex Sweeney]

https://github.com/kaiarasanen/lean4-collatz-proof-template

[Michael Rothgang]

My first impression of the README is "this looks LLM-generated". A proof of only 140 lines in Lean feels impossible to me: that cannot be true.

[Michael Rothgang]

Trying the code on the playground, it appears the line endings are unusual --- the server doesn't even start. Could this be why?

[Kyle Miller]

For some reason they removed mathlib from the lakefile in a commit that says "corrected lakefile.lean" https://github.com/kaiarasanen/lean4-collatz-proof-template/blob/main/lakefile.lean

[Aaron Liu]

definitely false, since they forgot to exclude zero

[Aaron Liu]

collatz doesn't reach one starting from zero

[Kyle Miller]

Has the module Mathlib.Data.Real.Log ever existed?

[Tristan Figueroa-Reid]

Kyle Miller said:

Has the module Mathlib.Data.Real.Log ever existed?

That's what I've been trying to figure out.

[Kyle Miller]

Apparently "mathlib4‑nightly (2025‑07‑13)" works on Lean 4.4.0 https://github.com/kaiarasanen/lean4-collatz-proof-template/blob/main/lean-toolchain

[Tristan Figueroa-Reid]

If I ignore some other errors, it seems that some of the norm_nums in this proof evaluate to False.

[Michael Rothgang]

Indeed, the very first one already does: 2 ≤ 3/2 (in real numbers) is not true. Oh wow.

[Michael Rothgang]

Another thing: once the imports are fixed, there are 32 errors in this file - this was clearly not built at all.

[Michael Rothgang]

This is even worse than the other LLM slop proofs that just stated a trivial definition, but at least built.

[Tristan Figueroa-Reid]

I'm surprised that this messed up the definition given that there's now a standard definition of these open problems. I was hoping that formal-conjectures would make proofs like this easier to ignore...

[Alex Sweeney]

Yikes. In their reddit thread they claimed to not use AI

[suhr]

Tristan Figueroa-Reid said:

I was hoping that formal-conjectures would make proofs like this easier to ignore...

That's not how it works. You need too add popular conjectures to mathlib + write some guidelines on how to use these definitions for proofs. (And even this won't really work, but at least makes it easier to filter such stuff...)

Right now there's only https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LSeries/RiemannZeta.html#RiemannHypothesis in mathlib. That's not enough!

[Ruben Van de Velde]

There's one good thing about this evolution. Not long ago, people would post inscrutable PDFs or blogs with their claims, and you'd need to actually read them to figure out it's nonsense. Now you can just point out that the code doesn't compile

[Eric Wieser]

Alex Sweeney said:

Yikes. In their reddit thread they claimed to not use AI

Maybe their AI was just claiming that it did not call out to any other AI system

[Eric Wieser]

Ruben Van de Velde said:

Now you can just point out that the code doesn't compile

Annoyingly these users often claim their code does compile, and then you have to explain "no, lake build didn't build your files because you didn't tell it about them"

[Notification Bot]

5 messages were moved from this topic to #general > Changing the default behavior of `lake build` by Eric Wieser.