Proof of the Collatz conjecture ?

Stream: new members

[tvscitechtalk]

I encountered this proof of the famous Collatz conjecture:

https://www.academia.edu/1595051/COLLATZ_CONJECTURE_PROOF

The Collatz Conjecture Proof

Cody T. Dianopoulos

(561)252-0803

merlincody@gmail.com

May 30, 2012

Abstract
The Collatz Conjecture, first posed in 1937 by Lothar Collatz, has finally been confirmed through a series of nested proofs by fifteen-year-old Cody T. Dianopoulos.

Now my questIon is: can we check that proof using the Lean theorem prover? I have no experience with the Lean theorem prover whatsoever (nor with any other theorem prover), so I need help how to set up the material proof presented in the paper so that Lean can check if that proof is correct.

Is there anyone here that can help me with that?
I would very much appreciate that !
COLLATZ_CONJECTURE_PROOF-1.pdf

[Mario Carneiro]

Yes, you can use an interactive theorem prover to validate the lines of a proof and find where the mistake in this proof is. If you have no prior experience with using lean, I would suggest #tpil or #mil to get started learning how to render mathematical claims in lean and prove things.

[Damiano Testa]

In fact, take a look at lemma 2 and see what is wrong with it.

[tvscitechtalk]

Damiano Testa zei:

In fact, take a look at lemma 2 and see what is wrong with it.

Can you give me a hint?

[tvscitechtalk]

Mario Carneiro zei:

Yes, you can use an interactive theorem prover to validate the lines of a proof and find where the mistake in this proof is. If you have no prior experience with using lean, I would suggest #tpil or #mil to get started learning how to render mathematical claims in lean and prove things.

For the moment I don’t know how to start, but I will take your advice

[Yagub Aliyev]

tvscitechtalk said:

Damiano Testa zei:

In fact, take a look at lemma 2 and see what is wrong with it.

Can you give me a hint?

Indeed, (2^4-1)/3=5 is not composite but 2^4 is an even power of 2. I think there are more important works waiting to be formalized.

[Matt Diamond]

I think it could be a decent exercise for learning Lean as long as @tvscitechtalk understands that this is unlikely to be some kind of breakthrough result

[Matt Diamond]

though formalizing a successful proof would probably be more fun

[tvscitechtalk]

Yagub Aliyev zei:

tvscitechtalk said:

Damiano Testa zei:

In fact, take a look at lemma 2 and see what is wrong with it.

Can you give me a hint?

Indeed, (2^4-1)/3=5 is not composite but 2^4 is an even power of 2. I think there are more important works waiting to be formalized.

Please explain a little further!

[Jireh Loreaux]

The point is that the claimed proof in that paper of the Collatz conjecture is not valid. That paper is not really worth your time as even the basic lemmas (e.g., Lemma 2) are obviously wrong, as the 2^4 example shows.

[Damiano Testa]

Right:

• if the exponent is even, there are counterexamples,
• if the exponent is odd, the numerator is not divisible by 3, so talking about being "composite" is not especially meaningful.

[Kyle Miller]

I'm confused what Lemma 2 is even trying to say. I think it's saying that $k$ in $2^k$ is even, but even so, $k$ is even iff $2^k-1$ is divisible by $3$.

[Kyle Miller]

That's just Fermat's little theorem, though you don't need the full power of it for a fixed prime divisor like $3$.

[Kyle Miller]

What I don't see in Lemma 2 is a proof that $(2^k-1)/3$ is composite when $k$ is even. There can't be one though, because $k=4$ was already offered as a counterexample.

[Mauricio Collares]

I think they just meant "integer" instead of "composite", because the compositeness isn't used anywhere else. Stuff like "Since $\sum_{i=0}^k 4^i$ has no limit, it can be disregarded" is more suspicious. But personally I think some policy similar to https://meta.mathoverflow.net/questions/927/what-is-our-policy-on-asking-about-correctness-of-preprints should apply to this discussion.

[Damiano Testa]

Ah, I had interpreted the last "even" as referring to the exponent of 2! Either way, this statement needs more work.

[Damiano Testa]

Here the convention is probably to ask for a #mwe, I guess.

[Damiano Testa]

(Which I probably should have done, instead of opening the pdf...)

[Alex Kontorovich]

I sincerely hope that this isn't my fault... These days, when someone sends me their Collatz proof, I say that I'll be happy to look at it once it's formalized in a theorem prover....

[Alex Kontorovich]

Actually there are a few (serious) people who have asked me whether Mochizuki can be checked (or shown to be flawed) with Lean. I said, sure, if Mochizuki will offer his time and energy to the project (the way Scholze did), answering every stupid little question... (I highly doubt that would happen...)

[llllvvuu]

Maybe this guy should have dropped $1m on the Lean community instead https://www.scientificamerican.com/article/1-million-will-go-to-the-mathematician-who-busts-the-abc-conjecture-theory/

[Alex Kontorovich]

The Mathlib community is certainly welcome to take up that challenge! I highly doubt people here will choose to waste their time without somebody like Mochizuki (or someone who claims to understand the proof) leading the charge... (There are much easier ways to earn $1m...)

[tvscitechtalk]

What I would like to learn is: how I can transfer the proof from the paper into Lean using the specific language that Lean uses, so that Lean can work out if that proof is correct or not.
As an absolute beginner in Lean I can sure use some help with that ! The goal for me is learn how to use Lean on this specific problem !

[tvscitechtalk]

Matt Diamond zei:

I think it could be a decent exercise for learning Lean as long as tvscitechtalk understands that this is unlikely to be some kind of breakthrough result

tvscitechtalk

What I would like to learn is: how I can transfer the proof from the paper into Lean using the specific language that Lean uses, so that Lean can work out if that proof is correct or not.
As an absolute beginner in Lean I can sure use some help with that ! The goal for me is learn how to use Lean on this specific problem !

[Johan Commelin]

@tvscitechtalk Just start with an ordinary Lean tutorial. There's plenty of learning material out there. No reason to jump straight into a hard project.

[Jireh Loreaux]

@tvscitechtalk what I'm advocating for is that you don't try to transfer the proof from that paper into Lean. The reason is that learning to formalize is hard enough as it is without the added complexity of trying to formalize something that's incorrect! You should start with a tutorial, like Johan suggests, and after that, try to formalize something that is already known to be true and from a trusted source (like a textbook; these aren't error-free, but generally the errors are relatively small and can be avoided without too much headache).

[Junyan Xu]

maybe start with #nng ...

[Junyan Xu]

And I guess Mochizuki needs to develop his own proof assistant that implements "the essential logical structures".

[Mauricio Collares]

@tvscitechtalk The person who's explaining things to Lean needs to understand the proof in detail (in this case, probably enough to be sure of its correctness). In this sense, you will work out the correctness of the proof, not Lean. Where Lean saves time is that, once the proof is written down, other people can just trust Lean instead of trusting the author.