No non-trivial cycles exist in the Collatz conjecture

Stream: new members

[Lionel Laurore]

Hi everyone! :wave: I'm Lionel, a mathematician/computer scientist. I've recently published a proof that no non-trivial cycles exist in the Collatz conjecture (extending Garner's 1981 approach via simple induction). Paper: Advances in Pure Mathematics (2025), DOI: 10.4236/apm.2025.156018 Link: https://www.scirp.org/journal/paperinformation?paperid=143316 Main result: σ(s)=ω(s) for all n∈ℕ (where ω is Garner's coefficient stopping time). This directly implies no non-trivial cycles can exist. I'm new to Lean but very interested in formalizing this proof. I've started the Natural Number Game and understand the basics. Key lemma to formalize: Sequences s and 2^n·m+s have identical dynamics for the first n iterations, which enables a simple induction proof. Questions: 1. Would anyone be interested in collaborating on this formalization? 2. What's the best approach for formalizing an induction-based argument like this? Looking forward to learning from this community! Best, Lionel

[Notification Bot]

A message was moved here from #new members > Ortogonal projection of point onto line/plane/etc. by Ilmārs Cīrulis.

[Notification Bot]

A message was moved here from #new members > Ortogonal projection of point onto line/plane/etc. by Ilmārs Cīrulis.

[Kevin Buzzard]

@Lionel Laurore you are claiming a major result and the proof is not in a major journal (in fact it is in a journal which charges $699 in publishing fees), so it is probably not unreasonable for the null hypothesis still to be that there might be an error in the work. It is thus probably too premature to ask for a Lean formalization of the work. The way to make progress here is first to make what we in this community call a formal blueprint of the work, which is a document which is far longer than the paper and contains every single detail of all the arguments. But this is something which you should do yourself, before trying to recruit volunteers from this community.

[Kevin Buzzard]

An example of a formal blueprint is here. It is a hybrid LaTeX/Lean document, but the LaTeX part comes first, and the LaTeX part is a carefully-documented and complete proof, containing full details or precise references for every assertion made. The way to get going with this is to use the Lean Project template here https://github.com/leanprover-community/LeanProject and follow the instructions in the README. You have a long way to go before you're ready to write Lean code; what the community needs first is a LaTeX blueprint, which should be written by you as the person who understands the argument.

The risk of launching straight into Lean code is that then you end up with thousands of lines of Lean code which will become worthless if an error is found in the argument and the error cannot be fixed. But the process of discovering the error is essentially always found in the blueprint phase of the formalization process, rather than in the actual writing of the Lean code. In my experience, it's not Lean that finds the errors, it's the humans preparing the way.

[Lionel Laurore]

@Kevin Buzzard. Thank you for your reply. I should clarify that my APM paper is a full-length article (about 40 pages in the published version) with complete definitions and detailed proofs.

In my initial message I only summarized the result, which may have given the impression that the work was short or informal. I fully understand that a Lean blueprint would require a much more granular document, which is indeed a separate step.

I appreciate your explanation of the community standards.

[Bbbbbbbbba]

Lionel Laurore said:

identical dynamics

What does "identical dynamics" mean? Does it just mean that the terms at the same position are either both odd or both even?

[Kevin Buzzard]

Discussion of the proof is definitely off-topic on this forum. Feel free to take it to DMs.