Discovering Collatz Invariants Beyond LLMS: VICReg Regularization and Lean Verification

The Collatz conjecture (3x+1 problem) remains unsolved despite decades of computational and mathematical effort. Recent AI systems (AlphaProof, Aristotle) excel at syntactic proof manipulation but fail when structural discovery precedes formalization. We present a VICReg-based neuro-symbolic framework that combines: (1) a VICReg-regularized CNN-MLP regressor optimized for invariant extraction on chaotic systems, (2) a falsifiable validation protocol (R6/R7) with strict out-of-distribution splits and SMT-based falsification, and (3) a modular Lean 4 formalization separating proven theorems from empirical axioms. Our contributions: (a) VICReg-R7 achieves RMSE 443 on 120-160 bit numbers (vs. 947-1243 for baselines, -53-64%), (b) empirical rule Rule4b-K256 validated on 100 OOD numbers (seed 2026, 100% validation, enrichment 19.8), (c) three deterministic bound theorems formally proven in Lean (CollatzCore.lean, EXIT=0), (d) modular architecture explicitly separating "concrete" (proven theorems) from "wood" (empirical frontier). This work establishes a reproducible methodology for AI-assisted exploration of open problems, where learned correlations are transformed into verifiable mathematical hypotheses through automated falsification and formal proof.