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 (au sens de la densité logarithmique). 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 (in the sense of logarithmic density). 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 (vérifié sous Lean 4.27.0, Mathlib v4.27.0 ; no_cycle_k_le_1322 revérifié sous Lean 4.34.0 les 20 et 21/10/2026) — il ne prouve pas la conjecture de Collatz. Démontré : aucun cycle non trivial avec k ≤ 1322 (k = nombre de termes impairs), sous les hypothèses H1 BakerSeparation (hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme, voir mea culpa #28) et H2 BarinaVerification (traduction d'un résultat de calcul publié, Bařina 2025, n < 271). La 3e hypothèse, H3 DerivedLargeKBound (k > 1322 ⇒ n < 271), est supposée, non dérivée ; sous H2, elle équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque) (erratum du 2 octobre 2026 ; voir HYPOTHESES.md, section H3, qui la présente comme une dérivation : c'est corrigé par cet erratum). Le site documente aussi des énoncés sur les limites de certaines méthodes, par exemple δ8 : la chaîne Product-Bound ne peut pas, à elle seule, fermer les grands cycles. A conditional theorem formalized in Lean 4 (checked on Lean 4.27.0, Mathlib v4.27.0; no_cycle_k_le_1322 re-checked on Lean 4.34.0 on 20–21 October 2026) — it does not prove the Collatz conjecture. Proved: no non-trivial cycle with k ≤ 1322 (k = number of odd terms), under hypotheses H1 BakerSeparation (working hypothesis, stronger in this form than published effective bounds, see mea culpa #28) and H2 BarinaVerification (encoding of a published computational result, Barina 2025, n < 271). The 3rd hypothesis, H3 DerivedLargeKBound (k > 1322 ⇒ n < 271), is assumed, not derived; under H2 it is equivalent to the conclusion itself (in Lean, k is any return time) (erratum of 2 October 2026; see HYPOTHESES.md, section H3, which presents it as a derivation: corrected by this erratum). The site also documents statements about the limits of some methods, e.g. δ8: the Product-Bound chain cannot, on its own, close large cycles.

Lean 4 est un assistant de preuve formelle (proof assistant) ; le projet Lean a été lancé par Leonardo de Moura à Microsoft Research. Si le noyau (kernel) accepte une preuve, le raisonnement est correct à partir des hypothèses données — à condition que le vérificateur lui-même n'ait pas de bug (c'est arrivé : bug lean4#14576, juillet 2026). Il reste aussi à vérifier que les hypothèses ne contiennent pas déjà la réponse : c'est exactement l'erreur corrigée sur ce site le 2 octobre 2026. Mathlib est sa bibliothèque mathématique standard (v4.27.0 pour le preprint d'avril ; v4.34.0 pour les formalisations d'octobre et la revérification de no_cycle_k_le_1322). Lean 4 is a formal proof assistant; the Lean project was started by Leonardo de Moura at Microsoft Research. If the kernel accepts a proof, the reasoning is correct from the given hypotheses — provided the checker itself has no bug (it happened: bug lean4#14576, July 2026). One must also check that the hypotheses do not already contain the answer: that is exactly the error corrected on this site on 2 October 2026. Mathlib is its standard mathematics library (v4.27.0 for the April preprint; v4.34.0 for the October formalisations and the re-check of no_cycle_k_le_1322).

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 (il a déjà eu un bug : lean4#14576, corrigé dans Lean v4.32.2 le 28/07/2026) et aux axiomes utilisés. Notre théorème principal no_nontrivial_cycle_phase59 a été vérifié par le noyau de Lean 4.27.0 (Mathlib v4.27.0), avant cette correction, et n'a pas été revérifié depuis ; selon la référence expected_axioms.md, ses axiomes Lean sont propext, Classical.choice et Quot.sound. Ses trois hypothèses H1-H3 ne sont pas des axiomes Lean : ce sont des paramètres du théorème. 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 (it has had a bug: lean4#14576, fixed in Lean v4.32.2 on 28 July 2026) and in the axioms used. Our main theorem no_nontrivial_cycle_phase59 was checked by the Lean 4.27.0 kernel (Mathlib v4.27.0), before that fix, and has not been re-checked since; according to the reference expected_axioms.md, its Lean axioms are propext, Classical.choice and Quot.sound. Its three hypotheses H1-H3 are not Lean axioms: they are parameters of the theorem.

Le théorème dépend de trois hypothèses (H1 BakerSeparation, H2 BarinaVerification, H3 DerivedLargeKBound), qui sont des paramètres du théorème Lean. Ce n'est donc pas une preuve inconditionnelle de Collatz/Syracuse. De plus, H3 équivaut, sous H2, à la conclusion elle-même (en Lean, k est un temps de retour quelconque) : seul le cas k ≤ 1322 est démontré sans circularité, sous H1 et H2 (erratum du 2 octobre 2026). Pour situer : Hercher (2023) et la vérification de Bařina impliquent déjà qu'un cycle non trivial a au moins 1,375·10¹¹ termes impairs. The theorem depends on three hypotheses (H1 BakerSeparation, H2 BarinaVerification, H3 DerivedLargeKBound), which are parameters of the Lean theorem. It is therefore not an unconditional proof of Collatz/Syracuse. Moreover, under H2, H3 is equivalent to the conclusion itself (in Lean, k is any return time): only the case k ≤ 1322 is proved without circularity, under H1 and H2 (erratum of 2 October 2026). For context: Hercher (2023) together with Barina's verification already implies that a non-trivial cycle has at least 1.375·10¹¹ odd terms.

Tao 2019 (densité logarithmique 1, méthodes analytiques), Krasikov-Lagarias (densité partielle), Eliahou-Steiner (structure des cycles, identité fondamentale), Knight 2026 (« Collatz high cycles do not exist »), Barina 2025 (vérification computationnelle), Hercher 2023 (aucun m-cycle non trivial avec m ≤ 91). Notre site documente le paradigme Baker+CF et ses limites structurelles. Tao 2019 (logarithmic density 1, analytic methods), Krasikov-Lagarias (partial density), Eliahou-Steiner (cycle structure, fundamental identity), Knight 2026 ("Collatz high cycles do not exist"), Barina 2025 (computational verification), Hercher 2023 (no non-trivial m-cycle with m ≤ 91). Our site documents the Baker+CF paradigm and its structural limits.

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

Eric Merle (ORCID 0009-0008-7940-402X), chercheur indépendant (France), avec l'aide d'assistants IA, et en collaboration ouverte avec Benjamin Macindoe depuis juillet 2026 (dépôt public commun). Des modèles de langage, notamment Claude (Anthropic), servent à la recherche bibliographique, au code, à la formalisation et à la relecture ; d'autres modèles ont servi ponctuellement à des relectures croisées. Leurs sorties sont revérifiées à la source ; elles peuvent se tromper, et l'ont fait (voir les mea culpa). Ces relectures ne sont pas un peer review. Eric Merle (ORCID 0009-0008-7940-402X), independent researcher (France), with the help of AI assistants, in open collaboration with Benjamin Macindoe since July 2026 (shared public repository). Language models, notably Claude (Anthropic), are used for literature search, code, formalization and review; other models were occasionally used for cross-review. Their outputs are re-checked at the source; they can be wrong, and have been (see the mea culpa). These reviews are not a peer review.

ARES v2 est le nom de notre méthode interne de vérification avant publication : chaque affirmation doit avoir une source primaire ou secondaire vérifiable, sans interpolation, et les incertitudes sont documentées (epistemic_status : verified, partial, external_unverified…). Chaque événement du research-ledger porte ces métadonnées. Cette méthode n'a pas empêché des erreurs (voir l'erratum du 2 octobre 2026 et les mea culpa) ; quand une erreur est trouvée, elle est corrigée et documentée publiquement. ARES v2 is the name of our internal pre-publication checking method: every claim must have a verifiable primary or secondary source, with no interpolation, and uncertainty is documented (epistemic_status: verified, partial, external_unverified…). Every event in the research-ledger carries these metadata. This method did not prevent errors (see the erratum of 2 October 2026 and the mea culpa); when an error is found, it is corrected and documented publicly.