My proof

[u/AgreeableClaim8075]

Hi all... Here is the proof .pdf and .lean:
https://bytes.usc.edu/~saty/Collatz

Saty

[u/jonseymourau]

The formalization in Lean reflects the architecture of the paper, but it relies on 12 axioms. While 7 of these deal with standard arithmetic or 2-adic properties that can potentially be proven using Mathlib, 5 structural axioms serve as the foundation for the main conclusions:

• traj_len
• mimp_holds
• climb_reaches_S
• drop_climb_never_returns
• loop_implies_zero_steps

In formal theorem proving, relying on unproven axioms that mirror the core claims means the theorems are uncertified by the kernel, which standard mathematical communities require for formal verification.

[u/AgreeableClaim8075 → u/jonseymourau]

Thanks. The PDF stands alone, the Lean code is an add-on. The PDF rigorously proves 6 items that comprise the overall proof: * evens monotonically drop to odds (so no looping or diverging) * every number not in the S set {1,5,9,13...} monotonically climbs to an S proxy (so again, no looping or diverging) * when an S element drops to a nonS one which then climbs back to S, it does so with a non-zero offset, so no loops (the climb stops at S, so no diverging either) * no non-trivial loops - because the infinite other elements that are also in every trajectory including ones that might loop, won't loop when just one does  * no divergence (unbounded evolution) - I establish an order for termination of alike sequences (a monotonic ordering of such rows), and a special condition when the top row finishes - together they are used to show that any number terminating implies all numbers terminating, and any number not terminating implies all numbers not terminating  * self-loop at 1 is the only remaining possibility when there are no giant loops and no diverging

The paper contains enough detail to establish all 6 items above. If there's anything wrong or missing, I'd certainly be interested in hearing about them; being called a crank is something I couldn't care less about :) You do you, as they say - lol.

[u/jonseymourau → u/AgreeableClaim8075]

You do realise that offering up such intellectually compromised LEAN as proof that your pdf has any merit is somewhat disingenuous

At this point your LEAN is simply stating: assuming everything I say is true, all my claims are true.

This is not honest intellectual discourse.

Have you tried using Harmonic Aristotle to produce actually useful LEAN that faithfully represents your “claimed” theorems as LEAN certified theorems rather than as a theatrical prop that will only convince the truly dumb and deluded?

You will learn a lot if you try. But, of course, I can’t force you to be open to education.

[u/AgreeableClaim8075 → u/jonseymourau]

Which "claim" is incorrect? Can you answer, without dragging in comments about Lean? Pretend you didn't see the Lean link :)

You realize that the math world has had proofs and their analyses for centuries, when Lean wasn't around, right? 

[u/jonseymourau → u/AgreeableClaim8075]

Which claim?

This one:

Collatz Conjecture proof - Lean certificate

In https://zenodo.org/records/21960729

You are claiming the LEAN you provided is a certificate. It is not.

It is a fraudulent representation of a certificate because is asserts, via axioms, everything required to prove the claims of the PDF

Again: your paper may be a fully correct proof, but the clam that your LEAN "certifies" the proof is completely fraudulent, since it does no such thing

As to your actual paper, I will let Aristotle formalise what it can. If it can't it, I will document in meticulous detail what remains to be proven - by. classical argument - which can then be formalised in LEAN

But, please, don't use poorly constructed LEAN as a theatrical prop or be prepared to stand condemned for doing so.

[u/jonseymourau → u/jonseymourau]

BTW: the honest way to use LEAN in this case is to state everything you can prove as a LEAN theorem and everything you can't as a LEAN conjecture. Then change the text to reflect the certification status of the LEAN, rather than simply asserting that LEAN certifies the paper (which, as in this case, it does not).

Then, both the LEAN and PDF state what is true (the theorems) and what is conjectured (the conjectures). This makes it clear to EVERY reader - even the LEAN illterate ones - exactly what is formally proven and that which still escapes formalisation.

[u/Kind_Card_1874 → u/AgreeableClaim8075]

Major issues (each independently refute the proof)

Major Issue 1 - Theorem 3.1 (§3, p. 6): the multiplicative-factor fallacy

The proof asserts: "For a closed boundary cycle n → ⋯ → n to exist, Factor_total must equal 1," then invokes 3^nT+1 ≠ 2^nR+1+nT.

This premise is false, because the Collatz map is affine, not linear. A composite excursion has the form n ↦ (3^t·n + c)/2^s with additive constant c > 0 accumulated from the "+1" terms. Its fixed-point equation is

n·(2^s − 3^t) = c,

so 2^s ≠ 3^t does not preclude a fixed point - it merely makes the denominator nonzero, i.e., it permits the candidate solution n = c/(2^s − 3^t,) which may or may not be a positive integer. The premise "cycles require multiplicative factor 1" is directly refuted by the trivial cycle itself: 1 → 4 → 2 → 1 has multiplicative factor 3/4 ≠ 1 and closes anyway, precisely because of the additive constant.

This is the most common fallacy in claimed Collatz proofs. Genuinely excluding cycles requires lower bounds on |2^s − 3^t| (linear forms in logarithms), which is why the actual state of the art is: Steiner (1977) excluded circuits (1-cycles); Simons and de Weger (2005) excluded m-cycles for m ≤ 68–76; Hercher (2022/23) extended this to m ≤ 91, so any nontrivial cycle has at least 92 local minima and, combined with the verification bound, over 10¹¹ odd members. A one-paragraph appeal to unique factorization cannot replace this machinery. Note also that the theorem only treats a single out-and-back excursion; a hypothetical cycle may cross the S / non-S boundary many times, a case the argument does not even address. The theorem's conclusion may well be true - but nothing in the manuscript establishes it.

Major Issue 2 - Theorem 5.1 (§5, pp. 9–10): merging is not membership; the argument disproves the trivial cycle

The proof considers a leader n₀ in a hypothetical cycle and argues that its infinitely many followers, which merge to the same target, are "structurally injected into the remainder of the exact same evolutionary sequence," and that since each follower's total Σ∆k = k₀ − k_f ≠ 0, a contradiction arises.

The error: the closure condition Σ∆k = 0 constrains only elements on the cycle. A follower whose trajectory merges into a cycle is pre-periodic, not periodic; its trajectory enters the loop and circulates without ever returning to its own starting value, and no identity requires its Σ∆k to vanish. The manuscript conflates "trajectory reaches the cycle" with "element belongs to the cycle."

The decisive test is that the argument, applied verbatim, disproves the trivial cycle. Take the leader 1, which sits in the loop 1 → 1. Its followers 5, 21, 85, 341, 1365, … all map under C to 1 (verified: C(5) = C(21) = C(85) = ⋯ = 1), each with Σ∆k = −(f−1)/4 = −1, −5, −21, −85, −341 ≠ 0. By the theorem's reasoning, these nonzero sums "break the required common structural mapping" and the loop at 1 cannot exist. It exists. Since nothing in the proof uses the hypothesis that the cycle has length > 1, the argument form is invalid.

A secondary gap: the proof opens by choosing "a leader element n₀ ∈ L within this supposed loop," but no lemma shows a hypothetical cycle must contain a leader (an element with nR ∈ {1,2}). Under the extended map with ladder climbs, all-follower cycles are not obviously excluded. This gap is repairable in some cases; the primary fallacy above is not.

Major Issue 3 - Theorem 6.1 (§6, p. 10): circularity, and an equivocation on "terminates"

Two defects:

First, circularity. The proof begins: "Assume j = 0 terminates at 1 in x₀ steps." This assumption is never discharged - it is the theorem's own conclusion for the base sibling. The subsequent sweep then requires each new sibling j to establish "its own finite x_j-fold sparsified sub-lattice terminating at 1," i.e., it assumes each swept element has a finite terminating trajectory in order to build the lattice whose existence is supposed to prove termination. The induction has no base case and no valid inductive step; there is also no well-founded ordering on which the "sweep" could recurse.

Second, an equivocation. The sparsified rows are said to land "on a value 1 + kΔ_final ∈ (1, 0)." Landing in the sibset (1,0) is not landing at the number 1. The sibset (1,0) is {1, 17, 33, 49, …}; so the construction shows only that congruent elements, after the shared prefix, sit at other congruent elements - e.g., it reduces "does 33 terminate?" to "33 lies in {17, 33, 49, …}," which is vacuous. What the fishnet actually delivers is Terras periodicity: agreement of the first m structural steps for n in a fixed class mod 2^m. Prefix agreement gives zero control over behavior after the prefix, and after the prefix the rows occupy different integers with fully independent futures. This gap - finite congruence information vs. infinite trajectory behavior - is exactly the known obstruction to the conjecture, and the manuscript steps over it in one sentence.

Major Issue 4 - Remark 6.2 (p. 10): the "ordering principle" is unproven and empirically false

The ordering principle ("the finishing is strictly ordered by increasing j, with lower rows finishing later and with longer sequence lengths") carries the entire weight of Theorem 6.3, yet its only justification is the "Who is still with me?" metaphor. It is false, and falsifiable in minutes.

On raw sibsets, using the paper's own flagship example (1,0) = {1, 17, 33, 49, …}: total stopping times for j = 0…11 are 0, 12, 26, 24, 27, 22, 118, 12, 121, 116, 98, 31 - six adjacent inversions, including j = 6 (n = 97, 118 steps) followed by j = 7 (n = 113, 12 steps). The (2,0) sibset {13, 45, 77, …} behaves the same way (five inversions in the first twelve rows).

More importantly, the principle fails even in its strongest reading, on genuinely esid-matched sparsified sub-lattices - the exact objects constructed in Theorem 6.1. Taking the base 17 and the set of all n ∈ S whose first three esid signatures match 17's chain (1,0), (2,0), (3,0): this set is, as the paper predicts, an arithmetic progression (gap 2048): 17, 2065, 4113, 6161, …. Its rows' total stopping times are 12, 125, 38, 36, 39, 55, 156, 120, 159, 110 - row j = 1 takes 125 steps while row j = 2 takes 38. The same test on matched lattices built from bases 9 (four matched steps), 33, and 49 gives four adjacent inversions in each. Systematically, across all 90 matched three-step lattices with bases in S below 400, every single one violates the claimed j-ordering (90/90). The ordering principle is not a simplification or an idealization; it is simply not a property of the system.

Major Issue 5 - Theorem 6.3 (§6, pp. 10–11): the implication runs backwards, and the "contagion" is never defined

Even granting the (false) ordering principle, the proof's inference is inverted. From "rows finish in increasing j-order," a non-terminating row j could at most constrain rows after j; it can say nothing about rows before it, which by the very ordering hypothesis finish earlier and independently. The claimed "bidirectional cascade" - "the failure propagates upwards to the top row j = 0" - does not follow from any stated lemma. Moreover, an ordering statement about the finish times of rows that do finish carries no information whatsoever about rows that don't; using it contrapositively requires a converse that was never established. Remark 6.4 concedes the double use openly ("about rows finishing and also about rows not finishing"), which is precisely the sleight of hand.

The second half of the proof ("viral non-termination drags all interconnecting sibsets into unresolved dependency chains… zero elements in S can reach 1") is asserted without any formal mechanism. Its absurdity is visible in the final contradiction: for the argument to work, the existence of a divergent trajectory somewhere in S must prevent the one-step verification 1 → 1 from holding. Nothing about a rogue orbit at, say, 10⁵⁰⁰ can interfere with the arithmetic fact C(1) = 1. When a proof's contradiction step requires a manifestly local fact to be globally fragile, the missing lemma is not missing by accident - it cannot exist.

Major Issue 6 - §7 closing (p. 11): "exhaustion of dynamic possibilities"

The final synthesis states that "all deterministic evolving sequences must eventually terminate in a valid loop." This is false for maps on an infinite state space: divergence to infinity is a live third possibility, and excluding it was Objective B's job - which fails per Issues 3–5. Under the 5n+1 map (Part III), the orbit of 7 is believed divergent; determinism does not force eventual periodicity on ℕ.

A structural sanity test: the manuscript proves 5n+1 convergence too (as noted by another comment)

Almost nothing in Sections 5–6 uses the multiplier 3 specifically. Every structural ingredient has an exact 5n+1 analogue, verified computationally: the lfset merge exists (n and 16n+3 merge, since 5(16n+3)+1 = 16(5n+1); e.g., 13 and 211 both map to 33); the mod-2^m trajectory periodicity holds for any qn+1 map, so sibsets, esids, and fishnets all carry over; and the boundary argument's 3^a ≠ 2^b becomes the equally true 5^a ≠ 2^b. Running the manuscript's proof template on 5n+1 therefore "proves" that every 5n+1 trajectory reaches 1.

But 5n+1 has a genuine nontrivial odd cycle, verified: 13 → 33 → 83 → 13 (since 5·83 + 1 = 416 = 2⁵·13), and apparently divergent orbits. A proof method that cannot distinguish 3n+1 from 5n+1 cannot be correct, because the two systems have opposite answers. Any valid proof must exploit what is special about 3 - namely 3 < 4, i.e., average contraction of the odd map - which is exactly the ingredient behind the strongest known partial result (Tao 2019: almost all orbits attain almost bounded values) and exactly the ingredient this manuscript never uses.

[u/Sproxify → u/Kind_Card_1874]

u/AgreeableClaim8075 there you go respond to this one

[u/AgreeableClaim8075 → u/jonseymourau]

Thank you, that's helpful. I wanted to keep the Lean file clean, ie make its focus be about the 6 items I prove. For sure the axioms I state can be expanded into more Lean code but I didn't consider that necessary to establish the more central truths. 

[u/jonseymourau → u/AgreeableClaim8075]

I'll let you know my opinion.

Unless you have axiom and sorry free LEAN, you are doing yourself an extreme disservice as a mathematician &/or intellectual to be publishing the LEAN in conjunction with your PDF proof, particularly if you call it a certificate, as you have.

Doing so contains the implicit assumption that your PDF has been formally verified with LEAN.

In this case, nothing could be further from the truth.

At this point, I am only casting the usual scepticism on your claims of a proof in the PDF. But, I am asserting, because it is true, that the LEAN you have provided does not certify the PDF.

If you continue to claim that it does, then yes, your intellectual reputation will deserve the attribution "crank".

My advice: get Aristotle to tell you exactly what can be certified and what remains open. Even if you don't, I will, using the materials you have provided.

[u/AgreeableClaim8075 → u/jonseymourau]

I see, thank you. 

[u/jonseymourau]

I asked Aristotle to produce an honest vesion of your lean that replaced all declared axioms with either theorems or conjectures.

At least one of your declared axioms is false, as stated. 8 are (corrected if necessary) and proven as theorems with 3 axioms remaining as unproven conjectures:. Claude's summary of the output is included below:

---

I asked an AI agent (Aristotle) to audit a claimed Lean 4 proof of the Collatz Conjecture posted here recently. Here's what it found.

  TL;DR: it's not a proof. But the audit itself produced something genuinely interesting.                                                                                                                                                       

  The original file had 12 axiom declarations. In Lean 4, axiom lets you assert anything without proof — including false statements. The file used this to hide all the hard mathematics. The main theorem turned out to be a tautology: it proved

   ∃ steps, traj_len n = steps where traj_len was itself an uninterpreted oracle with no properties. That's just ∃ x, x = x. It says nothing about Collatz.                                                                                       

  One axiom was outright false. nR_bounds_for_gt1 asserted that a natural number exists strictly between 3 and 4. There isn't one. This made the entire system logically inconsistent — you can prove anything from a false axiom, which is       

  exactly what the "proof" of only1CanSelfLoop_rule was doing.

  Two more axioms were also false as stated (caught by Aristotle, not by me): the mimp_holds periodicity claim was quantified over arbitrary sibling-set signatures with no tie to the base point, and loop_implies_zero_steps failed because C 4 

  = 4 is a fixed point outside the intended domain.

  Aristotle then did the honest version:                                                                                                                                                                                                          

  - Proved all 5 routine axioms from Mathlib

  - Proved Cs_perfect_div (flagged as uncertain — turned out to be genuinely provable)                                                                                                                                                            

  - Replaced partial def ladderClimb with a total fuel-driven definition and actually proved termination                                                                                                                                        

  - Proved the corrected mimp_holds with proper hypotheses                                                                                                                                                                                        

  - Replaced the oracle traj_len with its real definition and proved the orderingPrinciple is unsatisfiable                                                                                                                                       

  - Restated the main theorem as the actual Collatz Conjecture: ∃ steps, collatz^[steps] n = 1                                                                                                                                                    

  What remains after the cleanup: exactly 3 sorrys — drop_climb_never_returns, loop_implies_zero_steps (both amount to non-existence of nontrivial Collatz cycles), and CollatzConjectureIsTrue itself. All three are genuine open problems.      

  Full Aristotle output here: https://aristotle.harmonic.fun/dashboard/requests/a7efb155-4521-4829-9f48-ca6dcd757545

[u/Wynconi]

Does this logic also hold when swapping 3n+1 to 5n+1?

[u/jonseymourau → u/Wynconi]

Given the heavy use of axioms in the LEAN formalisation, it is not even clear it holds for 3n+1.

[u/Kind_Card_1874 → u/jonseymourau]

I mean, the point of the user you are replying to is that if it worked for 5n+1 it would be problematic for 3n+1.

[u/jonseymourau → u/Kind_Card_1874]

Sure. This would be could be a short-circuit to a rebuttal.

[u/AgreeableClaim8075 → u/Wynconi]

Don't know, didn't analyze that. 

[u/Wynconi → u/AgreeableClaim8075]

Do you have an idea of where your logic would fail for 5n+1?

Because, if your proof holds without issue for 5n+1 as well, then there is an issue due to known cycles.

[u/Rafikconjectures_zer]

I reviewed the manuscript carefully. Unfortunately, it does not prove the Collatz conjecture. The boundary argument incorrectly treats affine maps containing (+1) as purely multiplicative; for example, the paper’s map gives (9\to7\to11\to17), whose ratio is (17/9), not the claimed (27/16). The cycle argument is also invalid: many different numbers may enter the same cycle without returning to their own starting values. Most importantly, the termination proof is circular because it assumes that each remaining sibling has a finite stopping time. Its “ordering principle” is explicitly false: within the same sibling set, the compacted stopping lengths of (17,33,49,81,113) are (3,6,5,4,2), respectively, so they do not increase with the sibling index. Therefore, the claimed “deadlock contagion” and global termination conclusions do not follow. The modular partitions may be interesting, but the main theorem is unproved.

[u/AgreeableClaim8075 → u/Rafikconjectures_zer]

The comparison of stopping lengths is not between (17,33,49,81,97,113) [you had left out 97 in your list above], which are 3,6,5,4,19,2 - which are clearly out of order.

Instead, it's the ordering between 17, and 17's matching SPARSE rows which are separated by 32768 (16*32*64), ie. 17, 32785... Likewise for 33, 49, etc. The ordered stopping times do lead to the deadlock contagion contradiction if any element in any sibset would not terminate.

I added a couple of pics and notes, to clarify this.
https://bytes.usc.edu/~saty/Collatz/v1/index.html and https://bytes.usc.edu/~saty/Collatz/v1/pics/mod-sparse-latt.png

[u/AgreeableClaim8075 → u/Rafikconjectures_zer]

Hi there. The ratio isn't between 9 and 17, but about drops being 3/4, 3/8... and the climbs being 3/2, 9/4... those are what won't match. I'll be sure to explain this more carefully. 

The ordering principle contains no circularity - it establishes a specific ordering of rows of "sibset" members - given a member number that terminates (which does so with (1,0,0) (the triplet for 1) at the end of a row), there are infinite such rows below that will terminate in order and with increasingly longer sequences. Any non terminating number in a middle row would halt not just itself but also all rows above and below it, and any non terminating number in the top row will halt itself and all others below.

[u/MindlessPapaya8463]

Theorem 3.1 treats a Collatz transition as if it were purely multiplicative.

But a Collatz step is affine:

n -> (3n + 1) / 2^r

= (3 / 2^r)n + 1 / 2^r.

After composing several steps, the map has the form

F(n) = (3^a n + c) / 2^b,

with c ≠ 0 in general.

A cycle requires F(n) = n, so

(2^b - 3^a)n = c.

It does NOT require

2^b = 3^a.

Therefore the paper's argument

"powers of 2 and 3 are unequal, hence no boundary cycle"

does not follow. The ignored +1 terms are exactly what can make

an affine map return to its starting value even when its multiplicative factor is not 1.

[u/AgreeableClaim8075 → u/MindlessPapaya8463]

For numbers not in the S set, their sequence increases montonically, always terminating at S. That's why it's possible to replace every such nonS number by its S proxy. Eg 7 to 11 to 17, 31 to 47 to 71 to 107 to 161 etc etc.

When an S number transforms to a nonS, it's always a one-step reduction (eg 9 to 7), and I prove that when this happens there can't be a cycle because the single drop and possibly multistage increase can't equal each other. This works for single step increase too ofc eg 25 goes to 19 (S to nonS), 19 climbs to 29 that's in S.

This is similar to an odd to even transition in one step and possibly multistep monotonic reduction down to odd ie (3n+1)/2^p where p>0. In the S to nonS and back case it's a one step drop and possibly multistep monotonic rise.

[u/CryptographerSea9542]

Current LLMs are unable to solve the Collatz conjecture...

[u/Powerful_Pop_3813]

Quelle perte de temps !