What question did this study set out to answer?

The central aim is to provide a formal framework for the Collatz conjecture based on its structural properties.

May 22, 2026Open Access

Collatz Conjecture: A Formal Axiom System and Executable Framework Based on Structural Properties in Lean 4

Key Points

The central aim is to provide a formal framework for the Collatz conjecture based on its structural properties.
Implemented and verified the axiom system in the Lean 4 proof assistant.
Established key structural properties as provable theorems from standard integer axioms.
Utilized the Curry-Howard isomorphism for global convergence as an independent axiom.
The framework passes Lean's type-checker, ensuring the correctness of the implementation.
Demonstrated extensive empirical evidence and computational validation up to 2^71.
Offers a foundation for practical applications in cryptography and hardware design.

Abstract

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.

Collatz Conjecture: A Formal Axiom System and Executable Framework Based on Structural Properties in Lean 4

Key Points

Abstract

Cite This Study

Also Consider

Also Consider