ProofAtlas publishes Lean-verified code bounding the descent time of almost all Collatz trajectories

ProofAtlas publishes Lean-verified code bounding the descent time of almost all Collatz trajectories

On July 16, ProofAtlas published two formal declarations and linked them to a specific source code revision. One states that, for almost all positive starting values, the Collatz trajectory falls below a growing threshold within 436 · log N standard steps.

The Collatz problem defines a simple rule for an integer N: replace an odd number with 3N + 1, divide an even number by two, and repeat. The resulting sequence can grow for a long time, which makes it difficult to estimate when it will first fall substantially below its starting value.

Here, “almost all” has a precise meaning. Among the integers from 1 to X, the proportion of starting values whose trajectories make this descent approaches 100% as X grows. The threshold also grows with the starting value. For example, it can be set to √N. For almost all N, the trajectory will then fall below √N within 436 · log N steps. This constant counts every operation, including divisions by two.

The same file gives a bound of 145 · log N for the Syracuse iteration. After applying 3N + 1, this iteration immediately divides the result by every possible power of two until the next odd number is reached. The constants 436 and 145 cannot be compared directly: they use different methods for counting steps and apply to different sets of starting values.

In a 2019 paper, Terence Tao proved a result of the same type for logarithmic density: the trajectory of almost every starting value reaches any growing threshold. ProofAtlas has encoded a version for ordinary natural density and standard Collatz steps in code that can be inspected at a fixed revision.

The formal statement provides a precise basis for discussion. Instead of relying on a paraphrase of the result, one can inspect the theorem statement, the condition imposed on the threshold, and the method used to count steps.