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."

Un théorème conditionnel formalisé en Lean 4, kernel-checked (Mathlib v4.27.0) — ne prouve PAS la conjecture Collatz, mais établit la non-existence de cycles non-triviaux modulo 3 hypothèses externes documentées : BakerSeparation (conjecture de travail, renforcement non démontré des bornes Rhin/Wu/Salikhov publiées), BarinaVerification (n < 271, vérification computationnelle reproductible Barina 2025), DerivedLargeKBound (dérivation projet, k > 1322 ⇒ n < 271, combine Baker + fractions continues + Product Bound + Barina ; n'est pas un théorème publié — cf. HYPOTHESES.md §5). Plus une quadrilogie d'impossibilité conditionnelle (δ8, δ8', δ10, δ11) prouvant que cette conditionnalité est nécessaire dans le paradigme Baker+CF, pas arbitraire. A conditional theorem formalized in Lean 4, kernel-checked (Mathlib v4.27) — does NOT prove the Collatz conjecture, but establishes the non-existence of non-trivial cycles modulo 3 documented external hypotheses: BakerSeparation (working conjecture, undemonstrated strengthening of published Rhin/Wu/Salikhov bounds), BarinaVerification (n < 271, reproducible computational verification Barina 2025), DerivedLargeKBound (project-derived hypothesis, k > 1322 ⇒ n < 271, combines Baker + continued fractions + Product Bound + Barina; not a published theorem — see HYPOTHESES.md §5). Plus an impossibility quadrilogy (δ8, δ8', δ10, δ11 conditional) 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 — consultation indépendante de 3 modèles : Anthropic Claude Opus 4.7 (OLD3), Anthropic Claude Sonnet 4.6 (NEW4), OpenAI ChatGPT en mode raisonnement étendu (désigné « 5.5 » dans la nomenclature interne du protocole tri-IA, ne reflète pas la dénomination officielle publique d'OpenAI) — pour les décisions structurantes, et Two-Key validation (OLD3 ↔ NEW4) pour les contributions courantes. Ce protocole multi-IA est une discipline interne anti-hallucination ; il n'est PAS un peer review et ne remplace pas la vérification kernel-checked Lean 4. Eric Merle (ORCID 0009-0008-7940-402X), with a Three-Key validation multi-AI protocol — independent consultation of 3 models: Anthropic Claude Opus 4.7 (OLD3), Anthropic Claude Sonnet 4.6 (NEW4), OpenAI ChatGPT in extended reasoning mode (referred to as "5.5" in the internal tri-AI protocol nomenclature, does not reflect the official public OpenAI naming) — for structural decisions, and Two-Key validation (OLD3 ↔ NEW4) for routine contributions. This multi-AI protocol is an internal anti-hallucination discipline; it is NOT a peer review and does not replace the Lean 4 kernel-checked verification.

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.