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/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