What question did this study set out to answer?

January 16, 20260 citationsOpen Access

Finite-State Deterministic Validation of the Collatz Conjecture

Key Points

The aim is to formally validate the non-existence of non-trivial cycles and divergent trajectories in the Collatz system.
Utilized Lean 4 theorem prover for formal verification.
Developed a framework comprising 14 interconnected lemmas.
Established proof integrity with no unproven assertions.
Demonstrated structural impossibility of counterarguments.
Confirmed non-existence of cycles and divergence in the Collatz conjecture.
Established that the exponential cost of repair exceeds the linear budget of paths.
Achieved formal guarantees for all assertions made in the proof.

Abstract

This deposit contains a manuscript (preprint version) and its Lean 4 source code for the formal verification of the non-existence of non-trivial cycles and divergent trajectories in the Collatz system. The codebase implements a Deterministic Framework consisting of 14 interconnected lemmas (1A–2F) leading to the final contradictions in Theorem 1 (Non-Existence of Cycles) and Theorem 2 (Impossibility of Divergence). Verification Status: The entire formalization adheres to the highest standards of proof integrity: Tool: Lean 4 Theorem Prover / Mathlib. Integrity: The code contains zero unproven assertions (no uses of sorry or admit). Formal Guarantee: The synthesis formally validates that the required Exponential Cost of Repair (Corollary 1H-1) strictly exceeds the Linear Budget of the path, establishing the structural impossibility of both counterarguments to the conjecture. Note: No hidden axioms or unproven assumptions were used in the encoding of this proof. GitHub Badge (passing): https://github.com/adityabagchi2002-boop/LEAN-VALIDATED-PROOF-OF-COLLATZ-CONJECTURE/blob/main/README.md

问 AI

Bookmark

View Full Paper