Histoire de la conjecture
History of the conjecture
90 ans d'une question simple à formuler, toujours non résolue. Sources citées en bas de page. 90 years of a question simple to state, still unsolved. 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. Lagarias (1985) en retrace l'histoire.
German mathematician Lothar Collatz, two years after his PhD, describes the iteration n/2 or 3n+1 in personal notes. Lagarias (1985) recounts this history.
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 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 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.
Mesures d'irrationalité de logarithmes
Irrationality measures of logarithms
Rhin (1987), Wu (2003), Salikhov (2007) et Wu & Wang (2014) publient des mesures d'irrationalité ou d'indépendance linéaire de logarithmes de nombres rationnels (ln 2, ln 3). Exemples : Salikhov 2007 (mesure d'irrationalité de ln 3 : μ(ln 3) ≤ 5,125) ; Wu & Wang 2014 (μ(ln 3) < 5,117). C'est la tradition dont s'inspire notre hypothèse de travail H1 (BakerSeparation), plus forte que les bornes effectives publiées sous cette forme (mea culpa #28).
Rhin (1987), Wu (2003), Salikhov (2007) and Wu & Wang (2014) publish irrationality or linear-independence measures for logarithms of rational numbers (ln 2, ln 3). Examples: Salikhov 2007 (irrationality measure of ln 3: μ(ln 3) ≤ 5.125); Wu & Wang 2014 (μ(ln 3) < 5.117). This is the tradition behind our working hypothesis H1 (BakerSeparation), stronger in this form than published effective bounds (mea culpa #28).
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.
Tao : presque toutes les orbites bornées
Tao: almost all orbits bounded
Terence Tao publie Almost all orbits of the Collatz map attain almost bounded values, prouvant que pour presque tout (au sens de la densité logarithmique) entier n, l'orbite atteint des valeurs presque bornées. Plus grand pas vers la conjecture en 30 ans.
Terence Tao publishes Almost all orbits of the Collatz map attain almost bounded values, proving that for almost every (in the sense of logarithmic density) integer n, the orbit attains almost bounded values. Largest step toward the conjecture in 30 years.
Hercher : aucun m-cycle pour m ≤ 91
Hercher: no m-cycles with m ≤ 91
Christian Hercher établit qu'il n'existe aucun m-cycle non trivial avec m ≤ 91 : tout cycle hypothétique a au moins 92 minima locaux (m ≥ 92). Il montre aussi que, si la conjecture est vérifiée jusqu'à 3·269 (ce que couvre la vérification de Bařina, 271), tout cycle non trivial a au moins 1,375·1011 termes impairs. Ce n'est pas la source de notre hypothèse H3 (DerivedLargeKBound).
Christian Hercher proves that there is no non-trivial m-cycle with m ≤ 91: every hypothetical cycle has at least 92 local minima (m ≥ 92). He also shows that, if the conjecture is verified up to 3·269 (covered by Barina's verification, 271), every non-trivial cycle has at least 1.375·1011 odd terms. This is not the source of our hypothesis H3 (DerivedLargeKBound).
Calegari-Dimitrov-Tang : holonomie arithmétique
Calegari-Dimitrov-Tang: arithmetic holonomy
Frank Calegari, Vesselin Dimitrov et Yunqing Tang tirent de leurs « bornes d'holonomie arithmétique » des mesures effectives d'irrationalité et d'indépendance linéaire, et retrouvent des théorèmes diophantiens effectifs jusque-là accessibles par les formes linéaires en logarithmes de Baker (prépublication). Sans lien publié avec Collatz ; notée comme piste exploratoire A' dans notre cartographie. La piste CDT (P6) figure comme cul-de-sac dans le catalogue depuis le 29/04/2026 ; sa lecture a été close le 21/10/2026, sur le résumé seul (voir le registre). Frank Calegari, Vesselin Dimitrov and Yunqing Tang derive from their "arithmetic holonomy bounds" effective measures of irrationality and linear independence, and recover effective Diophantine theorems hitherto approachable by Baker's linear forms in logarithms (preprint). No published link with Collatz; noted as exploratory route A' in our cartography. The CDT lead (P6) has been listed as a dead end in the catalogue since 2026-04-29; its reading was closed on 2026-10-21, on the abstract only (see the ledger).
Barina vérifie n < 2^71
Barina verifies n < 2^71
David Barina publie une vérification calculatoire : tous les entiers n < 271 atteignent 1. Dans notre formalisation, ce résultat est traduit par l'hypothèse H2 BarinaVerification (un paramètre du théorème, pas un axiome Lean).
David Barina publishes a computational verification: every integer n < 271 reaches 1. In our formalization this result is encoded as hypothesis H2 BarinaVerification (a parameter of the theorem, not a Lean axiom).
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 un théorème conditionnel, no_nontrivial_cycle_phase59, qui prend trois hypothèses en paramètres : H1 BakerSeparation (hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme), H2 BarinaVerification (traduction d'un résultat de calcul publié, Bařina 2025, n < 271) et H3 DerivedLargeKBound. Erratum (2 octobre 2026) : H3 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). Ce qui est démontré sans circularité : aucun cycle non trivial avec k ≤ 1322 (k = nombre de termes impairs du cycle), sous H1 et H2 (no_cycle_k_le_1322). Vérifié par le noyau de Lean 4.27.0 (Mathlib v4.27.0), avant la correction du bug de noyau lean4#14576 (Lean v4.32.2, 28/07/2026). Les 20 et 21 octobre 2026, les 35 fichiers Lean de la release v1.0 qui forment la clôture des imports de Phase58PorteDeuxFinal.lean (qui contient no_cycle_k_le_1322) ont été revérifiés sous Lean 4.34.0, qui contient la correction de lean4#14576 : ils compilent, et no_cycle_k_le_1322 ne dépend que de propext, Classical.choice et Quot.sound. Phase59 à Phase63 et PhaseVIII, donc no_nontrivial_cycle_phase59, n'ont pas été revérifiés. Détails et limites : recheck-v4.34-2026-10-20. Preprint déposé sur Zenodo (DOI 10.5281/zenodo.19790405) ; la version v4 du dépôt Zenodo (20/10/2026, DOI 10.5281/zenodo.23496480) conserve le PDF d'origine et ajoute un erratum de 2 pages.
Eric Merle formalizes in Lean 4 a conditional theorem, no_nontrivial_cycle_phase59, which takes three hypotheses as parameters: H1 BakerSeparation (working hypothesis, stronger in this form than published effective bounds), H2 BarinaVerification (encoding of a published computational result, Barina 2025, n < 271) and H3 DerivedLargeKBound. Erratum (2 October 2026): H3 is assumed, not derived; under H2 it is equivalent to the conclusion itself (in Lean, k is any return time). What is proved without circularity: no non-trivial cycle with k ≤ 1322 (k = number of odd terms of the cycle), under H1 and H2 (no_cycle_k_le_1322). Checked by the Lean 4.27.0 kernel (Mathlib v4.27.0), before the fix of kernel bug lean4#14576 (Lean v4.32.2, 28 July 2026). On 20–21 October 2026, the 35 Lean files of release v1.0 that make up the import closure of Phase58PorteDeuxFinal.lean (which contains no_cycle_k_le_1322) were re-checked on Lean 4.34.0, which includes the fix of lean4#14576: they compile, and no_cycle_k_le_1322 depends only on propext, Classical.choice and Quot.sound. Phase59–63 and PhaseVIII, hence no_nontrivial_cycle_phase59, were not re-checked. Details and limits: recheck-v4.34-2026-10-20. Preprint deposited on Zenodo (DOI 10.5281/zenodo.19790405); version v4 of the Zenodo record (20 October 2026, DOI 10.5281/zenodo.23496480) keeps the original PDF and adds a 2-page erratum.
δ11 — lemme conditionnel autour de Salikhov 2007 (retiré le 20/10/2026)
δ11 — conditional lemma around Salikhov 2007 (withdrawn on 2026-10-20)
Eric Merle publie, sur une branche d'étude, le lemme delta11_salikhov_insufficient (Lean 4.27.0 / Mathlib v4.27.0), lié à Salikhov 2007 (mesure d'irrationalité de ln 3 : μ(ln 3) ≤ 5,125). Retiré le 20 octobre 2026. Il reposait sur la transposition au problème, qui porte sur log₂ 3, de la mesure d'irrationalité de ln 3 de Salikhov 2007, et sur un axiome ad hoc non tiré de l'article ; la borne de Salikhov n'étant établie qu'au-delà de hauteurs non explicites, aucun seuil explicite n'en découle (erratum de la version Zenodo v4, item 3 ; note de retrait). Le code reste consultable pour l'historique, mais ne doit plus être cité comme un résultat. Historique : δ11 est conditionnel (trois axiomes ad hoc : C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound) et repose sur une transposition de Salikhov 2007 (mesure de ln 3) au problème ; cette transposition ne tient pas. Vérifié sous Lean 4.27.0, non revérifié depuis. Mea culpa publics associés : #29 à #32. Tag v0.7.3-delta11.
Eric Merle publishes, on a study branch, the lemma delta11_salikhov_insufficient (Lean 4.27.0 / Mathlib v4.27.0), related to Salikhov 2007 (irrationality measure of ln 3: μ(ln 3) ≤ 5.125). Withdrawn on 20 October 2026. It rested on the transposition to the problem, which involves log₂ 3, of Salikhov's 2007 irrationality measure of ln 3, and on an ad hoc axiom not taken from the paper; since Salikhov's bound holds only beyond unspecified heights, no explicit threshold follows from it (erratum of the Zenodo v4 version, item 3; withdrawal note). The code remains available for the record but must no longer be cited as a result. History: δ11 is conditional (three ad-hoc axioms: C_Salikhov, C_Salikhov_pos, c_salikhov_upper_bound) and rests on a transposition of Salikhov 2007 (a measure for ln 3) to the problem; that transposition does not hold. Checked on Lean 4.27.0, not re-checked since. Related public mea culpa: #29 to #32. Tag v0.7.3-delta11.
Collaboration ouverte avec Benjamin Macindoe
Open collaboration with Benjamin Macindoe
Eric Merle et Benjamin Macindoe (chercheur indépendant) ouvrent un dépôt public commun : un registre de résultats vérifiés indépendamment des deux côtés, par pull requests. Eric Merle and Benjamin Macindoe (independent researcher) open a shared public repository: a ledger of results checked independently on both sides, through pull requests.
Halbeisen–Hungerbühler 1997, Lagarias 1990 et Steiner 1978 en Lean ; version v4 du preprint, avec un erratum
Halbeisen–Hungerbühler 1997, Lagarias 1990 and Steiner 1978 in Lean; version v4 of the preprint, with an erratum
Eric Merle publie la formalisation en Lean 4.34.0 d'un article classique, Halbeisen–Hungerbühler 1997 (pas un résultat nouveau), puis celle de Lagarias 1990 (Acta Arith. 56) et, le 21/10, celle d'un théorème de Steiner 1978 (démontré ici sous l'hypothèse nommée H_Rhin, jamais un axiome, et sans hypothèse pour au plus 20 000 termes impairs ; elle n'apporte rien de nouveau sur les cycles de Collatz ; les énoncés et la preuve ont été écrits sans l'article original (Congr. Numer. 20, 1978), à partir de Steiner 1981, de la bibliographie annotée de Lagarias et de Simons–de Weger 2005 (lu dans sa version 1.44 de 2010), puis comparés à l'article, lu après la release v1.2 sur une copie numérisée ; rien ne change dans les fichiers Lean), toutes trois proposées sur ccchallenge et archivées sur Zenodo (DOI 10.5281/zenodo.23514572 pour Lagarias ; DOI 10.5281/zenodo.23498096 pour Halbeisen–Hungerbühler ; DOI 10.5281/zenodo.23541611 pour Steiner). La version v4 du preprint (DOI 10.5281/zenodo.23496480) garde le PDF d'avril et ajoute un erratum de 2 pages : démontré sans circularité, aucun cycle non trivial avec k ≤ 1322, sous H1 et H2. Le 27/10, la release v1.3 du dépôt Lean (DOI 10.5281/zenodo.23686224) ne change que la documentation et les métadonnées : elle consigne le retrait, daté du 21/10, de l'affirmation selon laquelle l'article de Steiner n'avait pas pu être consulté. Du 22 au 27/10 (v0.10.11 à v0.10.15), les 21 pistes du catalogue encore marquées « stub » ont été tranchées, chacune avec sa source ou sa raison : toutes sont des culs-de-sac, certaines retirées. Le 28/10, le dossier logs23/ (release v1.4, DOI 10.5281/zenodo.23720217) démontre le théorème de Steiner sans l'hypothèse H_Rhin, par une minoration bien plus faible qui suffit ; H_Rhin lui-même n'est pas démontré, et aucune nouveauté n'est revendiquée.
Eric Merle publishes a Lean 4.34.0 formalisation of a classical paper, Halbeisen–Hungerbühler 1997 (not a new result), then of Lagarias 1990 (Acta Arith. 56) and, on 21 October, of a theorem of Steiner 1978 (here proved under the named hypothesis H_Rhin, never an axiom, and without any hypothesis for at most 20,000 odd terms; it proves nothing new about Collatz cycles; the statements and the proof were written without the original paper (Congr. Numer. 20, 1978), from Steiner 1981, Lagarias's annotated bibliography and Simons–de Weger 2005 (read in their version 1.44 of 2010), then compared with the paper, read after release v1.2 in a scanned copy; nothing in the Lean files changes), all three submitted to ccchallenge and archived on Zenodo (DOI 10.5281/zenodo.23514572 for Lagarias; DOI 10.5281/zenodo.23498096 for Halbeisen–Hungerbühler; DOI 10.5281/zenodo.23541611 for Steiner). Version v4 of the preprint (DOI 10.5281/zenodo.23496480) keeps the April PDF and adds a 2-page erratum: proved without circularity, no non-trivial cycle with k ≤ 1322, under H1 and H2. On 27 October, release v1.3 of the Lean repository (DOI 10.5281/zenodo.23686224) changes only the documentation and metadata: it records the withdrawal, dated 21 October, of the statement that Steiner's paper could not be accessed. From 22 to 27 October (v0.10.11 to v0.10.15), the 21 leads of the catalogue still marked "stub" were settled, each with its source or its reason: all are dead ends, some of them withdrawn. On 28 October, the logs23/ folder (release v1.4, DOI 10.5281/zenodo.23720217) proves Steiner's theorem without the hypothesis H_Rhin, through a much weaker lower bound that suffices; H_Rhin itself is not proved, and no novelty is claimed.
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.
- Wu, Q. (2003). On the linear independence measure of logarithms of rational numbers. Math. Comp. 72. DOI 10.1090/S0025-5718-02-01442-4.
- Salikhov, V. Kh. (2007). On the irrationality measure of ln 3. Doklady Mathematics 76(3), 955-957. DOI 10.1134/S1064562407060361.
- Wu, Q., Wang, L. (2014). On the irrationality measure of log 3. J. Number Theory 142, 264-273. DOI 10.1016/j.jnt.2014.03.007.
- Tao, T. (2019). Almost all orbits of the Collatz map attain almost bounded values. arXiv:1909.03562.
- Hercher, C. (2023). There are no Collatz m-Cycles with m ≤ 91. Journal of Integer Sequences 26, Article 23.3.5. arXiv:2201.00406. (Not the source of our hypothesis H3
DerivedLargeKBound, which is assumed, not derived — see the erratum of 2 October 2026.) - Barina, D. (2025). Improved verification limit for the convergence of the Collatz conjecture. J. Supercomputing 81(7), art. 810. DOI 10.1007/s11227-025-07337-0. (Encoded as hypothesis H2
BarinaVerification.) - Calegari, F., Dimitrov, V., Tang, Y. (2025). Arithmetic holonomy bounds and effective Diophantine approximation. arXiv:2510.04156.
- Merle, E. (2026). On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions. Preprint, Zenodo. DOI 10.5281/zenodo.19790405. (Version v4 of the Zenodo record (20 October 2026, DOI 10.5281/zenodo.23496480) keeps the original PDF and adds a 2-page erratum; see the erratum of 2 October 2026.)
Méthodologie : les affirmations 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). La plupart des autres affirmations (1972+) renvoient aux publications citées ci-dessus ; l'entrée 1996 s'appuie sur Wikipedia.
Methodology: historical claims 1937-1960s rely on secondary sources (Lagarias 1985, Wikipedia). Epistemic status partial for Hasse → Syracuse and Kakutani → US attributions (oral transmissions). Most other claims (1972+) refer to the publications cited above; the 1996 entry relies on Wikipedia.