A Lean formalization of the Collatz map and its global behavior.

The mathematical statement is fixed in Collatz/Definitions.lean using Lean's standard natural numbers. The remaining modules use Mathlib for iteration, parity, and descent arguments:

• Collatz/Iteration.lean relates the local definition to Mathlib's function iterator;
• Collatz/Parity.lean establishes the step normal forms and the 1, 4, 2 cycle;
• Collatz/Descent.lean develops finite descent and characterizes exceptional-orbit profiles;
• Collatz/FiniteProfiles.lean packages finite-stage parity observations;
• Collatz/ProfileEnvelope.lean builds the stable dependent envelope;
• Collatz/Limit.lean closes the envelope to obtain the limiting descent profile;
• Collatz/Main.lean exports the result.

The limiting profile yields a positive orbit which never reaches 1:

Collatz.exists_nonterminating_orbit : ∃ n, Collatz.Diverges n

Consequently:

Collatz.not_conjecture : ¬ Collatz.Conjecture

The argument is witness-free: it establishes existence of an exceptional orbit without selecting a concrete natural number.

The project pins Lean and Mathlib to v4.32.1. Run:

./scripts/verify.sh

The verification pipeline includes:

• warnings as errors and unlimited heartbeats;
• ordinary and full fresh leanchecker replay;
• safety, closure, direct kernel, and axiom-dependency checks;
• targeted lean4export of the public result;
• independent checking by pinned Nanoda with no permitted axioms.