H_Rhin itself is not proved, no novelty is claimed, and the formalisation proves nothing new about Collatz cycles.H_Rhin lui-même n'est pas démontré, aucune nouveauté n'est revendiquée, et la formalisation n'apprend rien de nouveau sur les cycles de Collatz.
steiner_cycle_nh · DOI 10.5281/zenodo.23720217 · Lean 4.34.0

Cartographie scientifique · Pré-publication

Ce site ne prouve pas la conjecture de Collatz. Le preprint d'avril 2026 a un erratum du 2 octobre 2026 ; ce qui est démontré, tel que publié : aucun cycle non trivial avec k ≤ 1322, sous les hypothèses H1 et H2. This site does not prove the Collatz conjecture. The April 2026 preprint has an erratum of 2 October 2026; what is proved, as published: no non-trivial cycle with k ≤ 1322, under hypotheses H1 and H2.

Une enquête sur les cycles non triviaux hypothétiques de la suite de Collatz, avec des formalisations en Lean 4.

Aussi connue en France sous le nom de Conjecture de Syracuse (« suite de Syracuse », « algorithme de Syracuse », « problème 3n+1 »). Also known as the Syracuse problem, the 3n+1 problem, the Kakutani problem, the Hasse algorithm, or the Ulam conjecture.

Formalisations en Lean 4 de trois travaux classiques sur les cycles de Collatz (Halbeisen–Hungerbühler 1997, Lagarias 1990, Steiner 1978), avec une note d'errata ; un catalogue de trente-six pistes, chacune avec sa fiche ; et le preprint d'avril 2026, avec son erratum.

Résultats · octobre 2026Results · October 2026

Formalisations en Lean 4 de travaux classiques

Lean 4 formalisations of classical work

Les énoncés sont figés dans des fichiers à part ; chaque énoncé démontré est vérifié par le noyau de Lean 4.34.0 avec les seuls axiomes standard, et revérifiable depuis un clone neuf. Rien de nouveau n'est revendiqué sur les cycles de Collatz, et ce site ne prouve pas la conjecture.Statements are frozen in separate files; each proved statement is checked by the kernel of Lean 4.34.0 with the standard axioms only, and can be re-checked from a fresh clone. Nothing new is claimed about Collatz cycles, and this site does not prove the conjecture.

Dernier jalonLatest milestone

Steiner 1978, sans hypothèseSteiner 1978, without hypothesis

2026-10-28

Le seul circuit des entiers positifs qui soit un cycle est {1, 2} : démontré en Lean 4 sans l'hypothèse H_Rhin (dossier logs23/). H_Rhin lui-même n'est pas démontré ; aucune nouveauté n'est revendiquée. The only circuit on the positive integers that is a cycle is {1, 2}: proved in Lean 4 without the hypothesis H_Rhin (folder logs23/). H_Rhin itself is not proved; no novelty is claimed.

Pour auditer →To audit → DOI (v1.4)DOI (v1.4)

Article de 1990Paper of 1990

Lagarias 1990Lagarias 1990

2026-10-20

60 énoncés figés, tous démontrés en Lean 4 ; deux théorèmes sous des hypothèses nommées (théorème des nombres premiers, Baker–Fel'dman), jamais des axiomes. 60 frozen statements, all proved in Lean 4; two theorems under named hypotheses (prime number theorem, Baker–Fel'dman), never axioms.

Pour auditer →To audit → DOI (v1.1)DOI (v1.1)

Article de 1997Paper of 1997

Halbeisen–Hungerbühler 1997Halbeisen–Hungerbühler 1997

2026-10-19

Tout ce que l'article démontre est vérifié par le noyau de Lean (70 énoncés) ; la borne 1/2 de la Remarque 1 (pour l > 1000), que l'article ne démontre pas, ne l'est pas non plus. Everything the paper proves is checked by the Lean kernel (70 statements); the bound 1/2 of Remark 1 (for l > 1000), which the paper does not prove, is not proved here either.

Pour auditer →To audit → DOI (v1.0)DOI (v1.0)

Note techniqueTechnical note

Note d'errataErrata note

2026-10-21

9 points relevés sur Halbeisen–Hungerbühler 1997 et 21 sur Lagarias 1990 en les formalisant, chacun vérifié par un théorème Lean ou un script ; aucun n'invalide un théorème formalisé. 9 points found in Halbeisen–Hungerbühler 1997 and 21 in Lagarias 1990 while formalising them, each checked by a Lean theorem or a script; none invalidates a formalised theorem.

Pour auditer →To audit →

Toutes les versions des releases Lean : DOI de concept 10.5281/zenodo.23498095 (dernière : v1.5, 28/10/2026). Cartes complètes : Papers.All versions of the Lean releases: concept DOI 10.5281/zenodo.23498095 (latest: v1.5, 2026-10-28). Full cards: Papers.

Travail récentRecent work

État des travaux

Snapshot d'activité du projet, traçable sur GitHub. Registre complet (Research Ledger) → Le preprint d'avril 2026 et son erratum du 2 octobre 2026 suivent juste après.

Cette section documente l'état du projet et sa traçabilité ; elle ne constitue pas une revendication d'acceptation ou de preuve finale. This section documents project status and traceability; it is not a claim of acceptance or final proof.

Dernier jalon

Steiner 1978 sans l'hypothèse H_Rhin (logs23/, v1.4)Steiner 1978 without the hypothesis H_Rhin (logs23/, v1.4)

2026-10-28

Le dossier logs23/ du dépôt Lean (release v1.4, archive Zenodo DOI 10.5281/zenodo.23720217) démontre, sans l'hypothèse H_Rhin, le théorème de Steiner 1978 sur les circuits : le seul circuit des entiers positifs qui soit un cycle est {1, 2}. Il prouve pour cela une minoration bien plus faible que H_Rhin, qui suffit ; H_Rhin lui-même n'est pas démontré, la borne est bien plus faible que les bornes publiées, aucune nouveauté n'est revendiquée, et la formalisation n'apprend rien de nouveau sur les cycles de Collatz. Jalon précédent : les 21 pistes « stub » du catalogue tranchées (27/10/2026). The logs23/ folder of the Lean repository (release v1.4, Zenodo archive DOI 10.5281/zenodo.23720217) proves, without the hypothesis H_Rhin, Steiner's 1978 theorem on circuits: the only circuit on the positive integers that is a cycle is {1, 2}. To do so it proves a lower bound much weaker than H_Rhin, which suffices; H_Rhin itself is not proved, the bound is far weaker than the published ones, no novelty is claimed, and the formalisation proves nothing new about Collatz cycles. Previous milestone: the 21 "stub" leads of the catalogue settled (2026-10-27).

→ logs23/ (9e42fa5)

Statut paper

Preprint — Zenodo (4 versions, avril–octobre 2026)Preprint — Zenodo (4 versions, April–October 2026)

PREPRINT 2026-10-20

« On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions ». Soumission au Journal of Automated Reasoning le 27/04/2026, rejetée le 13/05/2026 ; pas de nouvelle soumission. 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 : voir l'erratum. "On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions". Submitted to the Journal of Automated Reasoning on 2026-04-27, rejected on 2026-05-13; no new submission. 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.

→ DOI Zenodo

Dernière vérification Lean

Steiner 1978 sans H_Rhin : 14 énoncés vérifiés sous Lean 4.34.0Steiner 1978 without H_Rhin: 14 statements checked on Lean 4.34.0

2026-10-28

Dossier logs23/ (release v1.4) : 14 énoncés figés avant leurs preuves, tous prouvés ; 0 sorry dans les preuves, 0 native_decide, axiomes standard seuls (Lean 4.34.0, Mathlib v4.34.0) ; check.sh relancé le 28/10/2026 depuis un clone neuf du commit f9c33aa. Il prouve, sans H_Rhin, la minoration 1/(2^k − 1) ≤ |(k + l) log 2 − k log 3| pour tout k > 20 000 et tout l ≥ 0, et en déduit cinq des six énoncés de steiner1978/ qui supposaient H_Rhin. H_Rhin lui-même n'est pas démontré. Archive Zenodo (logiciel, v1.4) : DOI 10.5281/zenodo.23720217. Précédemment : steiner1978/, 12 énoncés, dont 6 sous l'hypothèse nommée H_Rhin, jamais un axiome (check.sh relancé depuis une compilation propre le 21/10/2026). Folder logs23/ (release v1.4): 14 statements frozen before their proofs, all proved; 0 sorry in the proofs, 0 native_decide, standard axioms only (Lean 4.34.0, Mathlib v4.34.0); check.sh run on 2026-10-28 from a fresh clone of commit f9c33aa. It proves, without H_Rhin, the lower bound 1/(2^k − 1) ≤ |(k + l) log 2 − k log 3| for every k > 20,000 and every l ≥ 0, and derives from it five of the six statements of steiner1978/ that assumed H_Rhin. H_Rhin itself is not proved. Zenodo archive (software, v1.4): DOI 10.5281/zenodo.23720217. Previously: steiner1978/, 12 statements, 6 of them under the named hypothesis H_Rhin, never an axiom (check.sh run from a clean build on 2026-10-21).

→ logs23/ (9e42fa5)

Dernier audit

Relecture adverse de la v0.10.20Adversarial review of v0.10.20

2026-10-28

Relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de la v0.10.20 (résultats en tête de l'accueil, bannière compacte, archives du printemps 2026, menu, page Papers), contre les sources disponibles. Audit précédent : relecture adverse des changements de la v0.10.19 (corrections de l'audit du 28/10/2026), 2026-10-28. Internal adversarial review, AI-assisted (not peer review), of the changes of v0.10.20 (results first on the home page, compact banner, spring 2026 archive, menu, Papers page), against the available sources. Previous audit: adversarial review of the changes of v0.10.19 (corrections from the audit of 2026-10-28), 2026-10-28.

→ changelog

Travaux en cours

Collaboration ouverte avec B. MacindoeOpen collaboration with B. Macindoe

2026-10-19

Dépôt public commun ; huit pull requests fusionnées, la dernière (round 18) le 19 octobre 2026 ; deux en cours de revue (rounds 19 et 20). Shared public repository; eight pull requests merged, the last (round 18) on 19 October 2026; two under review (rounds 19 and 20).

→ one-obstruction-three-faces

Preprint · avril 2026Preprint · April 2026

Le preprint d'avril 2026 et son erratum du 2 octobre

The April 2026 preprint and its erratum of 2 October

Erratum (2 octobre 2026). Ce qui est démontré, tel que publié : aucun cycle non trivial avec k ≤ 1322 (k = nombre de termes impairs du cycle), sous les hypothèses H1 (BakerSeparation) et H2 (BarinaVerification, vérification de Bařina jusqu'à 2⁷¹) — théorème no_cycle_k_le_1322. La troisième hypothèse, H3 (DerivedLargeKBound : « pour tout cycle avec k > 1322, n < 2⁷¹ »), est supposée, non dérivée. Sous H2, elle exclut à elle seule tout cycle non trivial, et pas seulement les grands : en Lean, k est un temps de retour quelconque, et tout multiple d'un temps de retour en est un (cycle_nSeq_multiples). Elle équivaut donc à la conclusion, comme ProductBoundThreshold, l'hypothèse qu'utilise le PDF (erratum de la version Zenodo v4, item 1). Le théorème no_nontrivial_cycle_phase59 n'apporte donc rien au-delà de k ≤ 1322. 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. Vérification machine : le théorème principal a été vérifié sous Lean 4.27.0 (Mathlib v4.27.0), avant la correction du bug du 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. Les six fichiers Lean de la pile commune avec B. Macindoe ont été revérifiés sous Lean 4.34.0 (artefact 9934df4, 23/09/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.

Erratum (2 October 2026). What is proved, as published: no non-trivial cycle with k ≤ 1322 (k = number of odd terms of the cycle), under hypotheses H1 (BakerSeparation) and H2 (BarinaVerification, Barina's verification up to 2⁷¹) — theorem no_cycle_k_le_1322. The third hypothesis, H3 (DerivedLargeKBound: "for every cycle with k > 1322, n < 2⁷¹"), is assumed, not derived. Under H2 it excludes every non-trivial cycle on its own, not only the large ones: in Lean, k is any return time, and every multiple of a return time is again one (cycle_nSeq_multiples). It is therefore equivalent to the conclusion, as is ProductBoundThreshold, the hypothesis used in the PDF (erratum of the Zenodo v4 version, item 1). The theorem no_nontrivial_cycle_phase59 therefore adds nothing beyond k ≤ 1322. Version v4 of the Zenodo record (20 October 2026, DOI 10.5281/zenodo.23496480) keeps the original PDF and adds a 2-page erratum. Machine checking: the main theorem was checked on Lean 4.27.0 (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. The six Lean files of the stack shared with B. Macindoe were re-checked on Lean 4.34.0 (artifact 9934df4, 23 September 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.

Résultat principal — preprint (DOI Zenodo) · erratum du 2 octobre 2026

Théorème conditionnel : aucun cycle Collatz non trivial avec k ≤ 1322, sous les hypothèses H1 et H2

⚠ Théorème CONDITIONNEL⚠ CONDITIONAL theorem — trois hypothèses, paramètres des théorèmes (pas des axiomes Lean) : BakerSeparation (H1 : hypothèse de travail, plus forte que les bornes effectives publiées sous cette forme — voir mea culpa #28), BarinaVerification (H2 : traduction d'un résultat de calcul publié, Bařina 2025, n<2⁷¹), DerivedLargeKBound (H3 : hypothèse supposée, non dérivée ; équivaut sous H2 à la conclusion elle-même (en Lean, k est un temps de retour quelconque) — HYPOTHESES.md, section H3 ; ce fichier la présente comme une dérivation : c'est corrigé par l'erratum du 02/10/2026). Ne prouve PAS la conjecture de Collatz. — three hypotheses, parameters of the theorems (not Lean axioms): BakerSeparation (H1: working hypothesis, stronger in this form than published effective bounds — see mea culpa #28), BarinaVerification (H2: encoding of a published computational result, Barina 2025, n<2⁷¹), DerivedLargeKBound (H3: assumed hypothesis, not derived; under H2 equivalent to the conclusion itself (in Lean, k is any return time) — HYPOTHESES.md, section H3; that file presents it as a derivation: corrected by the erratum of 2 Oct 2026). Does NOT prove the Collatz conjecture.

Les théorèmes no_cycle_k_le_1322 (sous H1, H2) et no_nontrivial_cycle_phase59 (sous H1, H2, H3) ont été vérifiés 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). no_cycle_k_le_1322 a été revérifié sous Lean 4.34.0, qui contient la correction de lean4#14576, les 20 et 21 octobre 2026 : il ne dépend que de propext, Classical.choice et Quot.sound ; no_nontrivial_cycle_phase59 ne l'a pas été. Profil d'axiomes du théorème principal : propext, Classical.choice, Quot.sound, selon la référence expected_axioms.md (Lean 4.27.0). Comme 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é (voir l'erratum).

Ce que le projet apportait en avril 2026 : une formalisation Lean de l'exclusion des cycles avec k ≤ 1322 (sous H1 et H2) et un catalogue documenté de pistes et d'obstructions. Le résultat mathématique est déjà contenu dans la littérature : Hercher (2023) et la vérification de Bařina impliquent qu'un cycle non trivial a au moins 1,375·10¹¹ termes impairs. Sept théorèmes centraux, une quarantaine de fichiers Lean ; chaîne principale reproductible via reproduce.sh (Lean 4.27.0).

→ Lire le preprint d'avril 2026 (PDF, sans l'erratum) → DOI Zenodo → Architecture de la preuve

2⁷¹

tout entier sous 2⁷¹ atteint 1

Bařina 2025 (J. Supercomputing 81)

m ≥ 92

minima locaux de tout cycle non trivial

Hercher 2023 (JIS 26, 23.3.5)

k ≤ 1322

cycles exclus par notre théorème Lean (sous H1, H2)

no_cycle_k_le_1322 · Lean 4.27.0

pistes cataloguées (plus aucune note à sourcer)

Région I + II + III

§ I

Catalogue des voies d'attaque

Catalogue exhaustif des approches mathématiques pour la non-existence des cycles non triviaux Collatz. Cliquez sur une ligne pour voir les détails. Transparence éditoriale : plus aucune entrée n'est en statut stub (note exploratoire en attente de sourçage formel, que le champ status_meta du JSON marquait explicitement, cf. assets/data/pistes.json). Les vingt et une qui l'étaient (C, E.4, F, J, K, M, R, H, H.1, H.2, I.1, N, O, P, Q, Q.bis, V, W, X, Y, Z) ont été tranchées les 22 et 27/10/2026 (source vérifiée, cul-de-sac motivé ou retrait) ; la raison figure dans leur fiche.

ID	Nom	Région	Statut	4-test	Lean	Source

§ II

Archives du printemps 2026

Spring 2026 archive

Sections d'avril et de mai 2026, conservées pour l'historique ; plusieurs phrases et chiffres y ont été corrigés depuis, certains sans date dans le texte (voir le changelog) ; elles ne décrivent pas l'état actuel du projet. Pages de la même époque : lemmes du preprint, architecture de la preuve, explorateur Λ.Sections from April and May 2026, kept for the record; several sentences and figures in them were corrected later, some without a date in the text (see the changelog); they do not describe the current state of the project. Pages from the same period: lemmas of the preprint, architecture of the proof, Λ explorer.

Le verrou Λ_{S,k} et le diagramme des paradigmes · avril 2026The Λ_{S,k} lock and the paradigm diagram · April 2026

Λ_{S,k}

Le verrou Λ_{S,k}

En avril 2026, quatorze des quinze paradigmes du diagramme ont été notés comme retombant sur la même obstruction diophantienne ; ce décompte date d'avril 2026 ; dans le catalogue, tranché du 22 au 27/10/2026, aucune source publiée n'a été trouvée pour cinq de ces pistes (C pour sa partie Fourier, I.1, J, R pour ses autocorrélations, et W) et « Schémas + Faltings » (piste K) est retiré depuis le 22/10/2026, faute de source ; elles sont en pointillé dans le diagramme :

$$\Lambda_{S,k} = S \log 2 - k \log 3$$

graph LR
    P1["Tao 2019 ergodique"] -->|"Haar 0 ≠ ∅"| LAMBDA
    P2["Kolmogorov-Chaitin"] -->|"K=O(log k)"| LAMBDA
    P3["Fourier Sturmien"] -.->|"slope log_2 3"| LAMBDA
    P4["Padé / Wu / Salikhov"] -->|"μ(ln 3) < 5,117 (Wu & Wang 2014)"| LAMBDA
    P5["Marcovecchio 2014"] -->|"μ_2 algébriques"| LAMBDA
    P6["Tropical (piste IA)"] -.->|"décroissance fine"| LAMBDA
    P7["Schémas + Faltings
✗ 2026-10-22"] -.-> LAMBDA
    P8["Néron-Tate"] -->|"ABC effective"| LAMBDA
    P9["Tresses / Nœuds"] -.->|"insensible 2/3-adique"| LAMBDA
    P10["Logique modèle"] -->|"Cobham 2 bases"| LAMBDA
    P11["Skolem-Mahler-Lech"] -->|"non-LRS"| LAMBDA
    P12["Anashin 2-adique"] -.->|"ergodicité ℤ_2"| LAMBDA
    P13["Krasikov-Lagarias"] -->|"densité aveugle"| LAMBDA
    P14["Holomorphic LSW"] --> LAMBDA
    P15["Inv. statistiques"] -.->|"autocorr. Christoffel"| LAMBDA

    LAMBDA["Λ_{S,k}
VERROU"]
    BAKER["H1 BakerSeparation
(paramètre — hypothèse de travail)"]
    BARINA["H2 BarinaVerification
Bařina 2025, n < 2^71"]
    DERIVED["H3 DerivedLargeKBound
(paramètre SUPPOSÉ)
k > 1322 → n < 2^71"]
    LE["no_cycle_k_le_1322
k ≤ 1322 · sous H1, H2"]
    GT["no_cycle_k_gt_1322
k > 1322 · H3 + H2
(circulaire, voir l'erratum)"]
    MAIN["no_nontrivial_cycle_phase59
Lean 4.27.0"]

    DELTA8["δ8
Product-Bound
impossibility · non formalisé
(remarque de HH 1997, §5)"]
    DELTA8P["δ8'
Baker+CF lower
not upper"]
    DELTA10["δ10 (Phase64)
retiré le 21/10/2026
(cartographie dépassée)"]
    DELTA11["δ11 (Phase65)
conditionnel · 3 axiomes ad hoc
retiré le 20/10/2026"]

    LAMBDA -->|"hypothèse H1"| BAKER
    BAKER --> LE
    BARINA --> LE
    BARINA --> GT
    DERIVED --> GT
    LE --> MAIN
    GT --> MAIN

    DELTA8 -.->|"Product-Bound ne ferme pas la fenêtre"| DERIVED
    DELTA8P -.->|"contexte"| DERIVED
    DELTA10 -.->|"contexte (retiré)"| BAKER
    DELTA11 -.->|"contexte (retiré)"| BAKER

    style LAMBDA fill:#c8a86a,color:#0e0f13,stroke:#fff,stroke-width:2px
    style BAKER fill:#6a9b7a,color:#0e0f13
    style BARINA fill:#6a9b7a,color:#0e0f13
    style DERIVED fill:#3a4a5a,color:#e0e6f0,stroke:#fb923c,stroke-width:2px,stroke-dasharray:5
    style LE fill:#f3d99c,color:#0e0f13,stroke:#c8a86a,stroke-width:3px
    style GT fill:#3a4a5a,color:#e0e6f0,stroke:#fb923c,stroke-width:2px,stroke-dasharray:5
    style MAIN fill:#6a9b7a,color:#0e0f13
    style DELTA8 fill:#3a4a5a,color:#e0e6f0,stroke:#6366f1,stroke-width:1px
    style DELTA8P fill:#3a4a5a,color:#e0e6f0,stroke:#6366f1,stroke-width:1px
    style DELTA10 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P7 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P3 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P6 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P9 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P12 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style P15 fill:#3a4a5a,color:#e0e6f0,stroke:#fbbf24,stroke-width:2px,stroke-dasharray:5
    style DELTA11 fill:#3a4a5a,color:#e0e6f0,stroke:#fb923c,stroke-width:2px,stroke-dasharray:5

→ Diagramme d'avril 2026, conservé pour mémoire. Toutes ses flèches vers le verrou Λ sont celles d'avril 2026 : des hypothèses de travail, pas des résultats. En pointillé : les pistes pour lesquelles le catalogue, tranché du 22 au 27/10/2026, n'a trouvé aucune source publiée (C pour sa partie Fourier, I.1, J, R pour ses autocorrélations, et W) et « Schémas + Faltings » (piste K, retirée). Pour chaque piste, sa fiche du catalogue dit ce qui tient ; en particulier, celles de F et de Z ne confirment pas non plus ce retour au verrou (F : les mesures de Marcovecchio portent sur un seul logarithme, pas sur la forme linéaire ; Z : pour les fonctions de Letherman, Schleicher et Wood, le multiplicateur d'un cycle est nul). Ce ne sont pas ces paradigmes qui alimentent le théorème, mais les hypothèses H1, H2 et H3 (paramètres). Seule la branche k ≤ 1322 (H1, H2) est démontrée sans circularité ; la branche k > 1322 repose sur H3, supposée (voir l'erratum).

Hypothèses A, A′, B et C sur la sortie, estimations subjectives · avril 2026Hypotheses A, A′, B and C on the exit, subjective estimates · April 2026

§ III

Trois hypothèses sur la sortie

Évolution des probabilités estimées (estimations subjectives de l'auteur, non calculées) au fil des cycles d'investigation (Cycle 0 → Cycle 2). La hausse de C reflète la convergence cumulative des paradigmes vers Λ_{S,k}.

Combinaison Baker+CF+Khinchin

Baker+CF+Khinchin combination

Probabilité finale : <5% — bloquée par δ8 (énoncé sur la méthode Product-Bound, non formalisé).

Final probability: <5% — blocked by δ8 (a statement about the Product-Bound method, not formalized).

Combinaison HORS-δ8 (holonomy)

δ8-FREE combination (holonomy)

Probabilité finale : 8-12% — voie de l'holonomie arithmétique (Calegari-Dimitrov-Tang), hors cadre Baker+CF.

Final probability: 8-12% — arithmetic holonomy route (Calegari-Dimitrov-Tang), outside the Baker+CF framework.

Estimation d'avril 2026. La piste qui la motivait (Calegari–Dimitrov–Tang, piste 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 : cul-de-sac en l'état (voir le registre).

Estimate from April 2026. The lead behind it (Calegari–Dimitrov–Tang, 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: dead end as things stand (see the ledger).

Téléportation hors domaine

Out-of-domain teleportation

Probabilité finale : 5-10% — 16 sur 16 culs-de-sac dans la Région II.

Final probability: 5-10% — 16 of 16 dead-ends in Region II.

Riemann-class (sortie inaccessible 2026)

Riemann-class (exit unreachable in 2026)

Probabilité finale : 75-80% — dominante après convergence δ8 + Cobham + 14 paradigmes.

Final probability: 75-80% — dominant after δ8 + Cobham + 14 paradigms convergence.

Estimation d'avril 2026. Le décompte de « 14 paradigmes » date aussi d'avril 2026 ; dans le catalogue, tranché du 22 au 27/10/2026, aucune source publiée n'a été trouvée pour cinq de ces paradigmes (pistes C pour sa partie Fourier, I.1, J, R pour ses autocorrélations, et W), et « Schémas + Faltings » (piste K) est retiré depuis le 22/10/2026, faute de source.

Estimate from April 2026. The count of "14 paradigms" also dates from April 2026; in the catalogue, settled from 22 to 27 October 2026, no published source was found for five of these paradigms (leads C for its Fourier part, I.1, J, R for its autocorrelations, and W), and "Schemes + Faltings" (lead K) has been withdrawn since 2026-10-22 for lack of a source.

δ8 — impossibilité Product-Bound

δ8 — Product-Bound impossibility

δ8 (impossibilité Product-Bound) — Pour fermer la fenêtre actuelle, la chaîne Product-Bound aurait besoin d'une minoration K·ln 2 − k·ln 3 > k^−c avec un exposant de forme linéaire c ≈ 0,96 (soit une mesure d'irrationalité μ = c + 1 ≈ 1,96). Or le théorème de Dirichlet impose c ≥ 1 (μ ≥ 2) : cette voie est fermée, quelle que soit la constante, avec une marge d'environ 0,04 sur l'exposant. C'est un énoncé sur une méthode de preuve : il n'exclut aucun cycle et n'est pas formalisé en Lean. Source : registre commun, entrée L-A9 (LEDGER.md ; convention corrigée en août 2026 ; l'énoncé du PDF Zenodo mélange les deux conventions). La conclusion rejoint une remarque de Halbeisen et Hungerbühler (Acta Arith. 78 (1997), §5, p. 238) : des estimations valables pour les cycles rationnels ne suffisent pas, seules, à exclure les cycles entiers. L'esquisse de preuve du Lemme 5.1 du PDF est retirée (erratum de la version Zenodo v4, item 7).

δ8 (Product-Bound impossibility) — To close the current window, the Product-Bound chain would need a lower bound K·ln 2 − k·ln 3 > k^−c with a linear-form exponent c ≈ 0.96 (i.e. an irrationality measure μ = c + 1 ≈ 1.96). Dirichlet's theorem forces c ≥ 1 (μ ≥ 2): this route is closed, whatever the constant, by a margin of about 0.04 in the exponent. This is a statement about a proof method: it excludes no cycle and is not formalized in Lean. Source: shared ledger, entry L-A9 (LEDGER.md; convention corrected in August 2026; the statement in the Zenodo PDF mixes the two conventions). The conclusion amounts to a remark of Halbeisen and Hungerbühler (Acta Arith. 78 (1997), §5, p. 238): estimates valid for rational cycles cannot on their own exclude integer cycles. The proof sketch of Lemma 5.1 in the PDF is withdrawn (erratum of the Zenodo v4 version, item 7).

Lemme R72 (Lean 4)

Lemma R72 (Lean 4)

Identité Steiner factorisée — pierre angulaire de l'arsenal.

Factored Steiner identity — cornerstone of the arsenal.

Lean 4.27.0 · arsenal-postjar/-- R72 NEW — identité Steiner factorisée :
    n · (2^S - 3^k) = corrSum n k.
    Universel : pour tout cycle `IsOddCycle n k`. -/
theorem cycle_n_mul_D_s_eq_corrSum
    (n k : ℕ) (hcyc : IsOddCycle n k) :
    n * ((2 : ℕ) ^ (aSumSeq n k) - 3 ^ k) = corrSum n k := by
  have h_steiner_nat : n * 2 ^ (aSumSeq n k) = 3 ^ k * n + corrSum n k :=
    steiner_cycle_eq n k hcyc
  have h_pow_gt : 2 ^ (aSumSeq n k) > 3 ^ k :=
    cycle_pow2_gt_pow3_universal n k hcyc
  have h_n_D_distrib : n * ((2 : ℕ) ^ (aSumSeq n k) - 3 ^ k) =
                       n * 2 ^ (aSumSeq n k) - n * 3 ^ k := by
    rw [Nat.mul_sub_left_distrib]
  rw [h_n_D_distrib, h_steiner_nat]
  have h_comm : 3 ^ k * n = n * 3 ^ k := by ring
  omega

Lemme R92 (Lean 4)

Lemma R92 (Lean 4)

Premier certificat fini case-by-case dérivé de l'arsenal lacunaire.

First finite case-by-case certificate derived from the lacunary arsenal.

Lean 4.27.0 · arsenal-postjar/-- R92 NEW — Showcase : pour cycle k=2 avec aSeq[0] ≡ 1 mod 3
    et aSeq[1] ≡ 1 mod 3, on a 7 ∤ D_s. -/
theorem cycle_k_2_parity_1_1_p_7_no_dvd_D_s
    (n : ℕ) (hcyc : IsOddCycle n 2)
    (h_s_0 : aSeq n 0 % 3 = 1)
    (h_s_1 : aSeq n 1 % 3 = 1) :
    ¬ (7 : ℕ) ∣ ((2 : ℕ) ^ (aSumSeq n 2) - 3 ^ 2) := by
  apply cycle_lacunary_nonzero_implies_p_nmid_D_s n 2 7 hcyc
  rw [orderOf_2_ZMod_7, orderOf_3_ZMod_7]
  have h_aS_0 : aSumSeq n 0 = 0 := by unfold aSumSeq aSum; simp
  have h_aS_1 : aSumSeq n 1 = aSeq n 0 := aSumSeq_one_eq n
  rw [Finset.sum_range_succ, Finset.sum_range_succ, Finset.sum_range_zero]
  simp only [zero_add]
  rw [h_aS_0, h_aS_1]
  simp only [show (2 - 1 - 0 : ℕ) = 1 from rfl, show (2 - 1 - 1 : ℕ) = 0 from rfl,
             show (1 % 6 : ℕ) = 1 from rfl, show (0 % 6 : ℕ) = 0 from rfl,
             show (0 % 3 : ℕ) = 0 from rfl, h_s_0]
  decide

Tests REQ-MATH · avril 2026REQ-MATH tests · April 2026

§ IV

Tests REQ-MATH-NNN exécutés

Scripts de contrôle numérique ponctuels. Seuls REQ-MATH-007 et REQ-MATH-012 sont publiés (branches d'étude du dépôt) ; les autres sont restés locaux. Ils vérifient des calculs précis ; ils ne valident pas toutes les affirmations du site.

§ V

Mea culpa publics

Chaque erreur détectée est documentée publiquement, avec une sévérité de 0 à 10 et la règle qui en est tirée. Aperçu de 16 mea culpa (numérotés jusqu'au #32).

§ VI

Communauté Collatz

Ressources et collaborations existantes autour de la conjecture de Collatz (vérifiées 2026-04-29).

ccchallenge.org

The Collatz Conjecture Challenge

Formalisation de la littérature Collatz, paper par paper. 358 papers à formaliser, forum GitHub Discussions + Discord communautaire.

Formalization of the Collatz literature, paper by paper. 358 papers to formalize, GitHub Discussions forum + community Discord.

→ ccchallenge.org

Terry Tao

What's new — blog

Blog WordPress de Terence Tao. Post 2019 fondateur : « Almost all Collatz orbits attain almost bounded values ».

Terence Tao's WordPress blog. Foundational 2019 post: "Almost all Collatz orbits attain almost bounded values".

→ terrytao.wordpress.com

Lagarias

The Ultimate Challenge — AMS 2010

Bibliographie annotée 1963-2009 par Jeffrey C. Lagarias (Univ. Michigan), curateur informel de la littérature Collatz.

Annotated 1963-2009 bibliography by Jeffrey C. Lagarias (Univ. Michigan), informal curator of the Collatz literature.

→ AMS Lagarias 3x+1 overview

tcosmo

coreli — Collatz Research Library

Bibliothèque Python (Jupyter) pour expérimentation et test d'hypothèses sur le processus de Collatz.

Python (Jupyter) library for experimentation and hypothesis testing on the Collatz process.

→ github.com/tcosmo/coreli

Quanta

Mathematician Proves Huge Result

Article de vulgarisation sur les avancées Tao 2019. Décembre 2019, Kevin Hartnett.

Popular-science article on the Tao 2019 advances. December 2019, Kevin Hartnett.

→ Quanta Magazine

Wikipedia

Collatz conjecture

Article complet, bibliographie, historique. Disponible en français et anglais.

Complete article, bibliography, history. Available in French and English.

→ Wikipedia

§ VII

Équipe

Ce projet est conduit par un chercheur indépendant, avec l'aide d'assistants IA, et en collaboration ouverte avec Benjamin Macindoe.

Investigateur principal

Principal Investigator

Eric Merle

Chercheur indépendant · France

Independent researcher · France

Conception, rédaction et formalisation Lean du projet. Auteur du preprint (DOI Zenodo 10.5281/zenodo.19790405). Les erreurs trouvées sont publiées (mea culpa, erratum).

Project design, writing and Lean formalization. Author of the preprint (Zenodo DOI 10.5281/zenodo.19790405). Errors found are published (mea culpa, erratum).

ORCID GitHub Email

Collaborateur · chercheur indépendant

Collaborator · independent researcher

Benjamin Macindoe

Collaboration ouverte depuis juillet 2026 : dépôt public commun et registre des résultats vérifiés des deux côtés. Auteur du preprint « Reduced coordinates for the Collatz map » (DOI 10.5281/zenodo.21730505) et du gateway interactif des cycles.

Open collaboration since July 2026: shared public repository and a ledger of results checked on both sides. Author of the preprint "Reduced coordinates for the Collatz map" (DOI 10.5281/zenodo.21730505) and of the interactive cycle gateway.

one-obstruction-three-faces Gateway Cycles

Outils

Tools

Assistants IA

AI assistants

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

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

Méthodologie

Methodology

Les affirmations sont vérifiées autant que possible par script et à la source ; quand une erreur est trouvée, elle est corrigée et documentée publiquement.

Claims are checked by script and at the source as far as possible; when an error is found, it is corrected and documented publicly.

Inspirations méthodologiques : Polymath Project (Tao, Gowers), Lean community (Mathlib), formalisation collaborative (ccchallenge.org).

Methodological inspirations: Polymath Project (Tao, Gowers), Lean community (Mathlib), collaborative formalization (ccchallenge.org).