In the past, many have attempted to prove the Collatz Conjecture using automated theorem provers such as Coq or Lean. However, most of these attempts were based on the commonly used "Collatz function":

f(n) = if n ≡ 0 (mod 2) then n/2 else 3n + 1

While this function captures the operation, it does not represent a structural mapping of the Collatz conjecture itself. In particular, it ignores the key non-cyclic nature of the conjecture’s convergence (e.g., the 4 → 2 → 1 loop), and lacks a precise formulation for building a global proof structure.

🧩 My Contribution:

I have proposed a two-stage exact mapping that decomposes the process into:

📘 A detailed explanation and proof outline is available in my preprint: Preprint Proving the Collatz Conjecture Using Infinite Axiom and Proo...

Preprint Exorcising the Collatz Conjecture with Classical Mathematics

❓ Question:

Given this new formulation, which explicitly defines the non-cyclic tree structure of the Collatz Conjecture, is it now feasible to verify the conjecture via automated theorem provers such as Coq or Lean, possibly using structural or strong induction over this tree?

I welcome feedback from anyone familiar with formal methods, inductive proof assistants, or structural number theory.

Best regards, Shinsuke Hamaji Independent Researcher, Japan [ORCID: https://orcid.org/0000-0002-3699-0363]