Histoire de la conjecture
History of the conjecture
90 ans d'une question simple à formuler, impossible à résoudre. Sources primaires citées en bas de page. 90 years of a question simple to state, impossible to solve. Primary sources cited at the bottom.
Lothar Collatz introduit le problème
Lothar Collatz introduces the problem
Le mathématicien allemand Lothar Collatz, deux ans après son doctorat, décrit l'itération n/2 ou 3n+1 dans des notes personnelles et lors de discussions à l'Université de Hambourg. Le problème ne sera publié qu'en 1985 par Lagarias.
German mathematician Lothar Collatz, two years after his PhD, describes the iteration n/2 or 3n+1 in personal notes and discussions at the University of Hamburg. The problem won't be formally published until Lagarias in 1985.
Helmut Hasse popularise le problème
Helmut Hasse popularizes the problem
Helmut Hasse, mathématicien allemand, présente le problème lors de visites en Amérique du Nord, notamment à Syracuse University (NY, USA) — d'où le nom Conjecture de Syracuse qui s'imposera en France. Le problème circule par transmission orale, gagnant le surnom Hasse's algorithm chez certains auteurs. Helmut Hasse, German mathematician, presents the problem during North American visits, notably at Syracuse University (NY, USA) — origin of the French name Conjecture de Syracuse. The problem spreads by oral transmission, gaining the nickname Hasse's algorithm in some sources.
Shizuo Kakutani diffuse aux États-Unis
Shizuo Kakutani spreads it in the US
Le mathématicien japonais Shizuo Kakutani aurait répandu le problème dans les universités américaines vers 1960, donnant le nom alternatif Kakutani's problem. Japanese mathematician Shizuo Kakutani reportedly spreads the problem in American universities ca. 1960, yielding the alternative name Kakutani's problem.
Conway prouve l'indécidabilité de la généralisation
Conway proves undecidability of the generalization
John H. Conway publie Unpredictable iterations et démontre que des généralisations naturelles du problème 3n+1 (fonctions FRACTRAN) sont Turing-complètes et donc indécidables. Ce résultat suggère que la conjecture de Collatz pourrait être intrinsèquement difficile.
John H. Conway publishes Unpredictable iterations and proves that natural generalizations of the 3n+1 problem (FRACTRAN functions) are Turing-complete and therefore undecidable. This result suggests Collatz could be intrinsically hard.
Crandall publie la première étude approfondie
Crandall publishes the first in-depth study
Richard E. Crandall publie On the "3x+1" problem, première analyse systématique des trajectoires, statistiques de stopping time, et tentatives de bornes inférieures sur les contre-exemples potentiels. Richard E. Crandall publishes On the "3x+1" problem, first systematic analysis of trajectories, stopping time statistics, and lower-bound attempts on potential counter-examples.
Lagarias publie le survey de référence
Lagarias publishes the reference survey
Jeffrey C. Lagarias publie The 3x+1 Problem and its Generalizations, l'article-survey qui établit la terminologie standard "3x+1 problem" et synthétise 50 ans de progrès. Reste la référence canonique 40 ans plus tard. Jeffrey C. Lagarias publishes The 3x+1 Problem and its Generalizations, the survey article that establishes the standard "3x+1 problem" terminology and synthesizes 50 years of progress. Still the canonical reference 40 years later.
Bryan Thwaites offre £1000
Bryan Thwaites offers £1000
Le mathématicien britannique Bryan Thwaites, qui a redécouvert le problème indépendamment, offre £1000 pour une preuve. Le problème est aussi connu sous le nom Thwaites conjecture en Grande-Bretagne. British mathematician Bryan Thwaites, who rediscovered the problem independently, offers £1000 for a proof. Also known as the Thwaites conjecture in the UK.
Bornes diophantiennes effectives
Effective Diophantine bounds
Rhin (1987), Wu (2003), Simons-de Weger (2005), Salikhov (2007) publient des bornes effectives sur les formes linéaires en logarithmes, type |S log 2 − k log 3| — outils techniques majeurs pour les approches Baker du problème de Collatz.
Rhin (1987), Wu (2003), Simons-de Weger (2005), Salikhov (2007) publish effective bounds on linear forms in logarithms, of the form |S log 2 − k log 3| — major technical tools for Baker-type approaches to Collatz.
Tao : presque toutes les orbites bornées
Tao: almost all orbits bounded
Terence Tao publie Almost all Collatz orbits attain almost bounded values, prouvant que pour presque tout (au sens de la densité naturelle 1) entier n, l'orbite atteint des valeurs presque bornées. Plus grand pas vers la conjecture en 30 ans.
Terence Tao publishes Almost all Collatz orbits attain almost bounded values, proving that for almost every (natural density 1) integer n, the orbit attains almost bounded values. Largest step toward the conjecture in 30 years.
Hercher : bornes locales sur m
Hercher: local bounds on m
Christoph Hercher établit que pour tout cycle hypothétique non-trivial, m ≤ 91 où m est le nombre de minima locaux dans la trajectoire impair-impair. Littérature contextuelle : cette borne sur m (minima locaux) porte sur une quantité distincte de k (pas impairs) et n'est pas la source de notre axiome DerivedLargeKBound, qui est une dérivation projet sur k (cf. HYPOTHESES.md §5 + §relation m vs k).
Christoph Hercher establishes that for any hypothetical non-trivial cycle, m ≤ 91 where m is the number of local minima in the odd-odd trajectory. Context literature: this bound on m (local minima) addresses a distinct quantity from k (odd steps) and is not the source of our DerivedLargeKBound axiom, which is a project-derived hypothesis on k (see HYPOTHESES.md §5 + §relation m vs k).
Calegari-Dimitrov-Tang : holonomie arithmétique
Calegari-Dimitrov-Tang: arithmetic holonomy
Approche alternative au paradigme Baker+CF : holonomie arithmétique. Différents outils, scope différent. Tracée comme Hypothesis A' dans notre cartographie (hors scope δ8). Alternative paradigm to Baker+CF: arithmetic holonomy. Different tools, different scope. Tracked as Hypothesis A' in our cartography (out of δ8 scope).
Barina vérifie n < 2^71
Barina verifies n < 2^71
David Barina publie la plus grande vérification computationnelle à ce jour : tous les n < 271 convergent vers 1. Référencé comme BarinaVerification dans notre formalisation.
David Barina publishes the largest computational verification to date: all n < 271 converge to 1. Cited as BarinaVerification axiom in our formalization.
Lean 4 : théorème conditionnel formalisé (ne prouve PAS la conjecture)
Lean 4: conditional theorem formalized (does NOT prove the conjecture)
Eric Merle formalise en Lean 4 (Mathlib v4.27) la non-existence de cycles non-triviaux conditionnellement à 3 hypothèses externes documentées : BakerSeparation, BarinaVerification, DerivedLargeKBound. Théorème principal no_nontrivial_cycle_phase59 kernel-checked. Trilogie initiale d'impossibilité (δ8, δ8', δ10) prouve formellement que cette conditionnalité est structurelle, pas arbitraire — étendue ultérieurement en quadrilogie avec δ11 (voir mai 2026). Preprint déposé sur Zenodo (28 pages, DOI 10.5281/zenodo.19790406).
Eric Merle formalizes in Lean 4 (Mathlib v4.27) the non-existence of non-trivial cycles conditional on 3 documented external hypotheses: BakerSeparation, BarinaVerification, DerivedLargeKBound. Main theorem no_nontrivial_cycle_phase59 kernel-checked. Initial impossibility trilogy (δ8, δ8', δ10) formally proves this conditionality is structural, not arbitrary — later extended into a quadrilogy with δ11 (see May 2026). Preprint deposited on Zenodo (28 pages, DOI 10.5281/zenodo.19790406).
δ11 — closure conditionnelle E.1 Salikhov 2007 + architecture 5-IA cross-validation
δ11 — conditional closure of approach E.1 Salikhov 2007 + 5-AI cross-validation architecture
Eric Merle ferme partiellement la piste E.1 du registre via le lemme delta11_salikhov_insufficient (Lean 4 / Mathlib v4.27) : Salikhov 2007 (μ ≤ 5.125) seul est insuffisant pour fermer la sous-branche k ∈ [3694, 3732], contrairement à Wu 2003. Théorème CONDITIONNEL sous 3 axiomes ad-hoc transparents (kernel-3 + C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound) — pas une dérivation directe du paper Salikhov 2007. Architecture 5-IA cross-validation (Claude Code + Claude Opus CLI + Gemini Pro 3.1 + ChatGPT 5.5 + Claude.ai web) : le cross-modèle a payé son prix DEUX FOIS (DOI Wu&Wang erroné catché par ChatGPT, axiome non-positivement-restreint catché par Gemini). 4 mea culpa publics #29 #30 #31 #32, score G3 final ~37/37 + 0 réserve. Build optimisé −82% (Phase 6-bis polish). Trilogie d'impossibilité étendue en quadrilogie conditionnelle (δ8, δ8', δ10, δ11). Tag v0.7.3-delta11.
Eric Merle partially closes approach E.1 of the registry via the delta11_salikhov_insufficient lemma (Lean 4 / Mathlib v4.27): Salikhov 2007 (μ ≤ 5.125) alone is insufficient to close the sub-branch k ∈ [3694, 3732], unlike Wu 2003. CONDITIONAL theorem under 3 transparent ad-hoc axioms (kernel-3 + C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound) — not a direct derivation from Salikhov 2007 paper. 5-AI cross-validation architecture (Claude Code + Claude Opus CLI + Gemini Pro 3.1 + ChatGPT 5.5 + Claude.ai web): cross-model paid its price TWICE (wrong Wu&Wang DOI caught by ChatGPT, non-positively-restricted axiom caught by Gemini). 4 public mea culpa #29 #30 #31 #32, final G3 score ~37/37 + 0 reservation. Optimized build −82% (Phase 6-bis polish). Initial impossibility trilogy extended into conditional quadrilogy (δ8, δ8', δ10, δ11). Tag v0.7.3-delta11.
Sources
Sources
- Wikipedia — Collatz conjecture (EN) · Conjecture de Syracuse (FR)
- Lagarias, J. C. (1985). The 3x+1 Problem and its Generalizations. American Math. Monthly 92(1), 3-23.
- Lagarias, J. C. (ed.) (2010). The Ultimate Challenge: The 3x+1 Problem. American Mathematical Society.
- Conway, J. H. (1972). Unpredictable iterations. Proc. Number Theory Conf., Boulder, 49-52.
- Crandall, R. E. (1978). On the "3x+1" problem. Math. Comp. 32(144), 1281-1292.
- Tao, T. (2019). Almost all Collatz orbits attain almost bounded values. arXiv:1909.03562.
- Hercher, C. (2023). Bounds on m for hypothetical non-trivial cycles, J. Integer Seq. 26.3.5. (Context literature only — not the source of
DerivedLargeKBound, which is a project-derived hypothesis on k; see HYPOTHESES.md §5.) - Barina, D. (2025). Convergence verification
n < 271. (Cited asBarinaVerification.) - Merle, E. (2026). On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4. Preprint, Zenodo. DOI 10.5281/zenodo.19790406.
Méthodologie ARES : claims historiques 1937-1960s reposent sur des sources secondaires (Lagarias 1985, Wikipedia). Statut épistémique partial pour les attributions Hasse → Syracuse et Kakutani → US (transmissions orales). Tous les autres claims (1972+) sont liés à des publications académiques vérifiables.
ARES methodology: historical claims 1937-1960s rely on secondary sources (Lagarias 1985, Wikipedia). Epistemic status partial for Hasse → Syracuse and Kakutani → US attributions (oral transmissions). All other claims (1972+) are tied to verifiable academic publications.