This repository provides a formal axiom system for the Collatz conjecture, fully implemented and verified in the Lean 4 proof assistant. Rather than pursuing a standard ZFC arithmetic derivation, this work establishes that key structural properties of the Collatz map—such as loop prohibition, a deterministic two-step contraction mechanism, and confluent orbit merging—are provable as sorry-free theorems from standard integer axioms. Utilizing the Curry-Howard isomorphism, global convergence is adopted as an independent axiom justified by extensive empirical evidence and computational validation up to 2^71. The resulting framework passes Lean's strict type-checker (CI-verified Green) and serves as an executable foundation for practical engineering applications, including bit-level mixing functions, hardware pipeline design, and non-linear cryptographic primitives. Distributed under the Apache License 2. 0.
Takeo Yamamoto (Thu,) studied this question.