Conditional theorem: no non-trivial Collatz cycle with k ≤ 1322, under H1 and H2 Théorème conditionnel : aucun cycle Collatz non trivial avec k ≤ 1322, sous H1 et H2 — erratum of 2 October 2026: the third hypothesis (H3) is assumed, not derived, and under H2 it is equivalent to the conclusion itself (in Lean, k is any return time) — erratum du 2 octobre 2026 : la troisième hypothèse (H3) est supposée, non dérivée, et sous H2 elle équivaut à la conclusion elle-même (en Lean, k est un temps de retour quelconque)

no_cycle_k_le_1322 · Lean 4.27.0 · re-checked on Lean 4.34.0 (20–21 Oct 2026)Lean 4.27.0 · revérifié sous Lean 4.34.0 (20 et 21/10/2026)

Cartographie scientifique · Pré-publication

Une enquête sur les cycles non triviaux conjecturés de la suite de Collatz, formalisée 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.

Trente-six pistes mathématiques, trois hypothèses (H1, H2, H3), une famille d'hypothèses ouvertes — organisées autour d'une obstruction diophantienne unique : l'inégalité de verrou reliant le nombre d'étapes impaires au nombre d'étapes paires d'un cycle hypothétique.

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 apporte : 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 paper (PDF) → 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

Λ_{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 est revu à la source dans le catalogue (« Schémas + Faltings », non sourcé, est retiré depuis le 22/10/2026) :

$$\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 DELTA11 fill:#3a4a5a,color:#e0e6f0,stroke:#fb923c,stroke-width:2px,stroke-dasharray:5

→ Les paradigmes du diagramme (liste d'avril 2026, en revue ; « Schémas + Faltings », retiré, en pointillé) convergent vers le verrou Λ ; ce ne sont pas eux 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).

§ 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

§ 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 ; il est revu à la source dans le catalogue, et l'un des paradigmes du diagramme (« Schémas + Faltings ») est retiré depuis le 22/10/2026, faute de source.

Estimate from April 2026. The count of "14 paradigms" also dates from April 2026; it is being reviewed against the sources in the catalogue, and one of the paradigms in the diagram ("Schemes + Faltings") 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]
  decide

§ 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

État des travaux

Snapshot d'activité du projet, traçable sur GitHub. Registre complet (Research Ledger) →

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

Les 21 pistes « stub » du catalogue tranchéesThe 21 "stub" leads of the catalogue settled

2026-10-27

Du 22 au 27/10/2026 (v0.10.11 à v0.10.15), les 21 pistes du catalogue encore marquées « stub » (notes exploratoires en attente de sourçage formel) ont été tranchées, chacune avec sa source vérifiée ou sa raison : toutes sont des culs-de-sac, certaines retirées. En chemin, le nom de la piste F, les fiches K et C, le mea culpa #23, la piste L, l'ancien texte de X et l'ancienne note de Z ont été corrigés (changelog v0.10.11, v0.10.12, v0.10.14 et v0.10.15). Jalon précédent : Steiner 1978 formalisé sous Lean 4.34.0 (21/10/2026) ; l'article original, lu ensuite, a été comparé aux énoncés : rien ne change dans les fichiers Lean. From 22 to 27 October 2026 (v0.10.11 to v0.10.15), the 21 leads of the catalogue still marked "stub" (exploratory notes pending formal sourcing) were settled, each with its checked source or its reason: all are dead ends, some of them withdrawn. Along the way, the name of lead F, entries K and C, mea culpa #23, lead L, the former text of X and the former note of Z were corrected (changelog v0.10.11, v0.10.12, v0.10.14 and v0.10.15). Previous milestone: Steiner 1978 formalised on Lean 4.34.0 (2026-10-21); the original paper, read afterwards, was compared with the statements: nothing in the Lean files changes.

→ changelog

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". 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". 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 : 12 énoncés vérifiés sous Lean 4.34.0Steiner 1978: 12 statements checked on Lean 4.34.0

2026-10-21

12 énoncés figés, tous prouvés, dont 6, parmi lesquels l'énoncé principal, sous l'hypothèse nommée H_Rhin, jamais un axiome ; axiomes standard seuls ; 0 sorry dans les preuves, 0 native_decide ; check.sh relancé depuis une compilation propre le 21/10/2026. Les énoncés et la preuve ont été écrits sans l'article original (Congr. Numer. 20, 1978) : ils sont reconstruits à 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). Après la release v1.2, le 21/10/2026, l'article a été lu sur une copie numérisée et comparé aux énoncés : rien ne change dans les fichiers Lean. Archive Zenodo (logiciel, v1.2) : DOI 10.5281/zenodo.23541611. Précédemment : la revérification de no_cycle_k_le_1322 sous Lean 4.34.0 (recheck-v4.34-2026-10-20). 12 frozen statements, all proved, 6 of them, including the main statement, under the named hypothesis H_Rhin, never an axiom; standard axioms only; 0 sorry in the proofs, 0 native_decide; check.sh run from a clean build on 2026-10-21. The statements and the proof were written without the original paper (Congr. Numer. 20, 1978): they are reconstructed from Steiner 1981, Lagarias's annotated bibliography and Simons–de Weger 2005 (read in their version 1.44 of 2010). After release v1.2, on 2026-10-21, the paper was read in a scanned copy and compared with the statements: nothing in the Lean files changes. Zenodo archive (software, v1.2): DOI 10.5281/zenodo.23541611. Previously: the re-check of no_cycle_k_le_1322 on Lean 4.34.0 (recheck-v4.34-2026-10-20).

→ steiner1978/ (057581a)

Dernier audit

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

2026-10-27

Relecture adverse interne, assistée par IA (ce n'est pas une évaluation par les pairs), des changements de la v0.10.16 (frise du registre, entrée d'octobre de la page Histoire, carte « Dernier jalon »), contre les sources disponibles. Audit précédent : relecture adverse des changements de la v0.10.15 (dernière piste « stub » du catalogue, retrait du test REQ-MATH-007, archivage de la bibliothèque prototype), 2026-10-27. Internal adversarial review, AI-assisted (not peer review), of the changes of v0.10.16 (ledger timeline, October entry of the History page, "Latest milestone" card), against the available sources. Previous audit: adversarial review of the changes of v0.10.15 (last "stub" lead of the catalogue, withdrawal of test REQ-MATH-007, archiving of the prototype library), 2026-10-27.

→ 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

§ VII

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

§ VIII

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