C'est un problème ouvert de théorie des nombres. Pour tout entier n ≥ 1, on itère la fonction T(n) = n/2 si n est pair, T(n) = 3n+1 si n est impair. La conjecture affirme que cette suite atteint toujours 1. Aucun contre-exemple connu, aucune preuve générale. Voir la page Syracuse pour la définition complète et les alias internationaux. It's an open number-theory problem. For every integer n ≥ 1, iterate the function T(n) = n/2 if n is even, T(n) = 3n+1 if n is odd. The conjecture states that this sequence always reaches 1. No counter-example known, no general proof. See the Syracuse page for full definition and international aliases.

Non (état 2026). Le résultat majeur récent est Tao 2019 : presque toutes les orbites de Collatz atteignent presque des valeurs bornées (densité naturelle 1). Vérification computationnelle : Barina 2025, n < 271. Aucune preuve inconditionnelle n'existe. No (as of 2026). Major recent result: Tao 2019 — almost all Collatz orbits attain almost bounded values (natural density 1). Computational verification: Barina 2025, n < 271. No unconditional proof exists.

Bryan Thwaites a offert £1000 en 1996 pour une preuve. Paul Erdős a dit "Les mathématiques ne sont pas prêtes pour ce problème" et a offert $500. Ce n'est pas un Millennium Prize Problem (Clay Institute, $1M réservés à 7 problèmes : Riemann, Yang-Mills, Navier-Stokes, etc.). Bryan Thwaites offered £1000 in 1996 for a proof. Paul Erdős said "Mathematics is not yet ripe for such questions" and offered $500. It is not a Millennium Prize Problem (Clay Institute, $1M reserved for 7 specific problems: Riemann, Yang-Mills, Navier-Stokes, etc.).

L'opération 3n+1 mélange multiplication par 3 et division par 2. Aucun outil arithmétique standard (théorie des nombres analytique, dynamique ergodique, théorie diophantienne) ne capture pleinement ce mélange. Conway 1972 a montré que des généralisations naturelles sont indécidables. Citation Erdős : "Mathematics is not yet ripe for such questions." The 3n+1 operation mixes multiplication by 3 and division by 2. No standard arithmetic tool (analytic number theory, ergodic dynamics, Diophantine theory) fully captures this mix. Conway 1972 showed that natural generalizations are undecidable. Erdős quote: "Mathematics is not yet ripe for such questions."

Une preuve formelle conditionnelle en Lean 4, kernel-checked (Mathlib v4.27.0), modulo trois hypothèses externes explicites : BakerSeparation (séparation diophantienne effective sur |S log 2 − k log 3|), BarinaVerification (n < 271), DerivedLargeKBound (Hercher 2023). Plus une trilogie d'impossibilité (δ8, δ8', δ10) prouvant que cette conditionnalité est nécessaire dans le paradigme Baker+CF, pas arbitraire. A conditional formal proof in Lean 4, kernel-checked (Mathlib v4.27.0), modulo three explicit external hypotheses: BakerSeparation, BarinaVerification, DerivedLargeKBound. Plus an impossibility trilogy (δ8, δ8', δ10) proving that this conditionality is necessary in the Baker+CF paradigm, not arbitrary.

Lean 4 est un assistant de preuve formelle (proof assistant) développé à Microsoft Research. Une preuve écrite en Lean 4 et acceptée par le noyau (kernel) est mathématiquement vérifiée à un niveau de rigueur supérieur à la peer review traditionnelle. Mathlib est sa bibliothèque mathématique standard (v4.27.0 utilisée ici). Lean 4 is a formal proof assistant developed at Microsoft Research. A proof written in Lean 4 and accepted by the kernel is mathematically verified to a level of rigor exceeding traditional peer review. Mathlib is its standard mathematics library (v4.27.0 used here).

Le noyau (kernel) Lean 4 est un petit programme qui vérifie chaque pas de preuve. Si le noyau accepte, la preuve est correcte modulo la confiance qu'on accorde à ce noyau et aux 3 axiomes minimaux Lean : propext, Classical.choice, Quot.sound. Notre théorème principal no_nontrivial_cycle_phase59 a été kernel-checked avec ces 3 axiomes seulement. The Lean 4 kernel is a small program that checks every proof step. If the kernel accepts, the proof is correct modulo trust in this kernel and Lean's 3 minimal axioms: propext, Classical.choice, Quot.sound. Our main theorem no_nontrivial_cycle_phase59 is kernel-checked with these 3 axioms only.

Le théorème dépend de trois hypothèses externes documentées (BakerSeparation, BarinaVerification, DerivedLargeKBound). Ce n'est donc pas une preuve inconditionnelle de Collatz/Syracuse. L'apport est de cartographier rigoureusement les obstructions structurelles qui rendent cette conditionnalité nécessaire, pas arbitraire. The theorem depends on three documented external hypotheses (BakerSeparation, BarinaVerification, DerivedLargeKBound). It is therefore not an unconditional proof of Collatz/Syracuse. The contribution is rigorously mapping the structural obstructions that make this conditionality necessary, not arbitrary.

Tao 2019 (densité presque-1, méthodes analytiques), Krasikov-Lagarias (densité partielle, sieve), Eliahou-Steiner (structure des cycles, identité fondamentale), Knight (méthodes de tamis), Calegari-Dimitrov-Tang 2025 (arithmetic holonomy — paradigme alternatif), Barina 2025 (vérification computationnelle), Hercher 2023 (bornes locales sur m). Notre site documente le paradigme Baker+CF et ses limites structurelles. Tao 2019 (near-1 density, analytic methods), Krasikov-Lagarias (partial density, sieve), Eliahou-Steiner (cycle structure, fundamental identity), Knight (sieve methods), Calegari-Dimitrov-Tang 2025 (arithmetic holonomy — alternative paradigm), Barina 2025 (computational verification), Hercher 2023 (local bounds on m). Our site documents the Baker+CF paradigm and its structural limits.

Code Lean 4 et paper sont open-source : GitHub repository (MIT pour le code, CC BY-SA 4.0 pour le site). Issues, pull requests, audits Red Team bienvenus. Le Research Ledger documente publiquement audits, mea culpa, corrections. Lean 4 code and paper are open-source: GitHub repository (MIT for code, CC BY-SA 4.0 for site). Issues, pull requests, Red Team audits welcome. The Research Ledger publicly documents audits, mea culpa, corrections.

Eric Merle (ORCID 0009-0008-7940-402X), avec un protocole Three-Key validation multi-IA (OLD3 + NEW4 + ChatGPT 5.5) pour les décisions structurantes, et Two-Key validation (OLD3 ↔ NEW4) pour les contributions courantes. Eric Merle (ORCID 0009-0008-7940-402X), with a Three-Key validation multi-AI protocol (OLD3 + NEW4 + ChatGPT 5.5) for structural decisions, and Two-Key validation (OLD3 ↔ NEW4) for routine contributions.

ARES v2 est notre méthodologie anti-hallucination multi-IA : 6 règles strictes pour vérifier toute claim avant publication, incluant la nécessité d'une source primaire ou secondaire vérifiable, l'absence d'interpolation, et la documentation des incertitudes (epistemic_status: verified | partial | external_unverified). Chaque event du research-ledger porte ces métadonnées. ARES v2 is our anti-hallucination multi-AI methodology: 6 strict rules to verify any claim before publication, including the need for a verifiable primary or secondary source, no interpolation, and documentation of uncertainty (epistemic_status: verified | partial | external_unverified). Every event in the research-ledger carries these metadata.