Steiner 1978 en Lean 4

Steiner 1978 in Lean 4

R. P. Steiner, « A theorem on the Syracuse problem », Congressus Numerantium 20 (1978), 553-559. C'est la formalisation d'un théorème classique de 1978, pas un résultat nouveau. La formalisation n'apporte rien de nouveau sur les cycles de Collatz. Le seul circuit sur les entiers positifs qui soit un cycle de l'application 3x+1 est {1, 2} : c'est démontré ici sous une hypothèse nommée, la borne de Rhin (H_Rhin, jamais un axiome), et sans aucune hypothèse pour au plus 20 000 termes impairs. 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. 12 énoncés figés, tous prouvés, 0 sorry dans les preuves, 0 native_decide (la vérification finie utilise decide +kernel), axiomes standard seuls (Lean 4.34.0, Mathlib v4.34.0). La borne pour 20 000 termes impairs n'utilise aucune vérification informatique de la conjecture, et elle est bien plus faible que les bornes qui en utilisent une (par exemple Hercher 2023) ; aucune nouveauté n'est revendiquée. Proposé sur ccchallenge (« Ready to be audited ») ; IA déclarée : Claude Opus 5.5 (Anthropic). Mise à jour (28/10/2026) : le dossier logs23/ (release v1.4) démontre ce théorème sans H_Rhin : il prouve une minoration bien plus faible, 1/(2^k − 1) ≤ |(k + l) log 2 − k log 3| pour tout k > 20 000 et tout l ≥ 0, qui suffit, et en déduit cinq des six énoncés qui supposaient H_Rhin (14 énoncés figés, tous prouvés, mêmes garanties). H_Rhin lui-même n'est pas démontré ; cette borne est bien plus faible que les bornes publiées (Laurent 1994 ; Laurent, Mignotte et Nesterenko 1995 ; Gouillon 2006). Code, script check.sh (relancé depuis une compilation propre le 21/10/2026) et correspondance avec les sources : steiner1978/ (057581a) ; sans hypothèse : logs23/ (9e42fa5) ; archive Zenodo (logiciel, v1.4) : DOI 10.5281/zenodo.23720217 (toutes versions : 10.5281/zenodo.23498095).

R. P. Steiner, "A theorem on the Syracuse problem", Congressus Numerantium 20 (1978), 553-559. This is the formalisation of a classical theorem from 1978, not a new result. The formalisation proves nothing new about Collatz cycles. The only circuit on the positive integers that is a cycle of the 3x+1 map is {1, 2}: it is proved here under a named hypothesis, Rhin's bound (H_Rhin, never an axiom), and without any hypothesis for at most 20,000 odd terms. 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. 12 frozen statements, all proved, 0 sorry in the proofs, 0 native_decide (the finite check uses decide +kernel), standard axioms only (Lean 4.34.0, Mathlib v4.34.0). The bound for 20,000 odd terms uses no computer verification of the conjecture, and it is far weaker than the bounds that do (for instance Hercher 2023); no novelty is claimed. Submitted to ccchallenge ("Ready to be audited"); AI declared: Claude Opus 5.5 (Anthropic). Update (2026-10-28): the logs23/ folder (release v1.4) proves this theorem without H_Rhin: it proves a much weaker lower bound, 1/(2^k − 1) ≤ |(k + l) log 2 − k log 3| for every k > 20,000 and every l ≥ 0, which suffices, and derives from it five of the six statements that assumed H_Rhin (14 frozen statements, all proved, same guarantees). H_Rhin itself is not proved; this bound is far weaker than the published ones (Laurent 1994; Laurent, Mignotte and Nesterenko 1995; Gouillon 2006). Code, check.sh script (run from a clean build on 2026-10-21) and comparison with the sources: steiner1978/ (057581a); without hypothesis: logs23/ (9e42fa5); Zenodo archive (software, v1.4): DOI 10.5281/zenodo.23720217 (all versions: 10.5281/zenodo.23498095).

Pour auditer : le README du dossier, section « Re-checking » (release v1.5) : énoncés figés, commande de revérification depuis un clone neuf, rapports d'axiomes enregistrés et écarts avec l'article (dossier steiner1978/ compris). logs23/README.md

To audit: the folder's README, section "Re-checking" (release v1.5): frozen statements, re-check command from a fresh clone, recorded axiom reports and differences from the paper (folder steiner1978/ included). logs23/README.md

Lagarias 1990 en Lean 4

Lagarias 1990 in Lean 4

J. C. Lagarias, « The set of rational cycles for the 3x+1 problem », Acta Arithmetica 56 (1990), 33-53 (DOI 10.4064/aa-56-1-33-53). C'est la formalisation d'un résultat classique de 1990, pas un résultat nouveau. 60 énoncés, tous prouvés (61 théorèmes : le Corollaire 2.1a est prouvé deux fois), 0 sorry dans les preuves, 0 native_decide, axiomes standard seuls (Lean 4.34.0, Mathlib v4.34.0). Le Théorème 3.1 avec la constante imprimée utilise le théorème des nombres premiers, et le Théorème 3.2 une conséquence de la borne de Baker–Fel'dman : ce sont des hypothèses nommées, jamais des axiomes. Le Théorème 3.1 est aussi prouvé sans hypothèse, avec la constante 6/5 au lieu de 5/4. Hors périmètre : les Théorèmes 3.3 et 4.3, et d'autres points listés dans le README. Les coquilles relevées sont listées à côté du texte imprimé (liste non exhaustive). Relectures adverses internes assistées par IA, jusqu'à deux passes consécutives sans remarque ; ce n'est pas une évaluation par les pairs. IA déclarée sur ccchallenge : Claude Opus 5.5 (Anthropic). Code et correspondance avec l'article : lagarias1990/ (e39566c) ; archive Zenodo (logiciel) : DOI 10.5281/zenodo.23514572. Note d'errata commune aux deux articles (Zenodo, 21/10/2026, DOI 10.5281/zenodo.23535498) : 21 points pour cet article, chacun vérifié par un théorème Lean ou par un script. Aucun n'invalide un théorème que nous avons formalisé. La liste n'est pas exhaustive. Les deux lignes fausses du tableau 3.1 (k = 35 et k = 73) étaient déjà corrigées dans l'OEIS (A102280, A102284 ; G. H. Morley, 2013).

J. C. Lagarias, "The set of rational cycles for the 3x+1 problem", Acta Arithmetica 56 (1990), 33-53 (DOI 10.4064/aa-56-1-33-53). This is the formalisation of a classical 1990 result, not a new result. 60 statements, all proved (61 theorems: Corollary 2.1a is proved twice), 0 sorry in the proofs, 0 native_decide, standard axioms only (Lean 4.34.0, Mathlib v4.34.0). Theorem 3.1 with the printed constant uses the prime number theorem, and Theorem 3.2 a consequence of the Baker–Fel'dman bound: these are named hypotheses, never axioms. Theorem 3.1 is also proved without any hypothesis, with the constant 6/5 instead of 5/4. Out of scope: Theorems 3.3 and 4.3, and other points listed in the README. The slips found are listed next to the printed text (the list is not exhaustive). Internal AI-assisted adversarial reviews, until two consecutive passes with no remark; this is not peer review. AI declared on ccchallenge: Claude Opus 5.5 (Anthropic). Code and comparison with the paper: lagarias1990/ (e39566c); Zenodo archive (software): DOI 10.5281/zenodo.23514572. Errata note common to both papers (Zenodo, 2026-10-21, DOI 10.5281/zenodo.23535498): 21 points for this paper, each checked by a Lean theorem or by a script. None of them invalidates a theorem that we formalised. The list is not exhaustive. The two wrong rows of Table 3.1 (k = 35 and k = 73) were already corrected in the OEIS (A102280, A102284; G. H. Morley, 2013).

Ce que vérifie le noyau, selon le README du dossier (en anglais) : « Section 2: Theorem 2.1, Corollaries 2.1a–b and the facts around them, the count (2.4)–(2.6) of irreducible cycles; Section 3: the 3x+k maps, the bijection with rational cycles, Theorems 3.1, 3.2, 3.4 and 3.5; Theorems 4.1 and 4.2 (4.2 with the printed constant 2n⁴); Tables 2.1 and 2.2; Table 3.1 as described below (48 printed rows, 2 corrected rows). »

What the kernel checks, according to the folder's README: "Section 2: Theorem 2.1, Corollaries 2.1a–b and the facts around them, the count (2.4)–(2.6) of irreducible cycles; Section 3: the 3x+k maps, the bijection with rational cycles, Theorems 3.1, 3.2, 3.4 and 3.5; Theorems 4.1 and 4.2 (4.2 with the printed constant 2n⁴); Tables 2.1 and 2.2; Table 3.1 as described below (48 printed rows, 2 corrected rows)."

Pour auditer : le README du dossier, section « How to check » (release v1.5) : énoncés figés, commande de revérification depuis un clone neuf, rapports d'axiomes enregistrés et écarts avec l'article. lagarias1990/README.md

To audit: the folder's README, section "How to check" (release v1.5): frozen statements, re-check command from a fresh clone, recorded axiom reports and differences from the paper. lagarias1990/README.md

Halbeisen–Hungerbühler 1997 en Lean 4

Halbeisen–Hungerbühler 1997 in Lean 4

L. Halbeisen et N. Hungerbühler, « Optimal bounds for the length of rational Collatz cycles », Acta Arithmetica 78 (1997), 227-239. C'est la formalisation d'un résultat classique de 1997, pas un résultat nouveau. Tout ce que l'article démontre est vérifié par le noyau de Lean, ainsi que la vérification finie de l'exemple du §4.4, que l'article faisait en partie par un calcul approché : si la conjecture est vérifiée jusqu'à 212 366 032 807 211, tout cycle d'entiers qui ne contient pas 1 a au moins 102 225 496 éléments. 70 énoncés figés avant leur preuve, 0 sorry dans les preuves, 0 native_decide, axiomes standard seuls (Lean 4.34.0, Mathlib v4.34.0). Non démontrée : la borne 1/2 de la Remarque 1 (pour l > 1000), que l'article ne démontre pas non plus. Écrit par Claude Opus 5.5 (Anthropic), recompilé à froid avant publication. Code, commande de vérification et correspondance ligne à ligne avec l'article : hh1997/ (36d5136). Archive Zenodo (logiciel) : DOI 10.5281/zenodo.23498096. Note d'errata commune aux deux articles (Zenodo, 21/10/2026, DOI 10.5281/zenodo.23535498) : 9 points pour cet article, chacun vérifié par un théorème Lean ou par un script. Aucun n'invalide un théorème que nous avons formalisé. La liste n'est pas exhaustive.

L. Halbeisen and N. Hungerbühler, "Optimal bounds for the length of rational Collatz cycles", Acta Arithmetica 78 (1997), 227-239. This is the formalisation of a classical 1997 result, not a new result. Everything the paper proves is checked by the Lean kernel, together with the finite verification behind the example of §4.4, which the paper did partly numerically: if the conjecture is verified up to 212,366,032,807,211, every cycle of integers not containing 1 has at least 102,225,496 elements. 70 statements frozen before their proofs, 0 sorry in the proofs, 0 native_decide, standard axioms only (Lean 4.34.0, Mathlib v4.34.0). Not proved: the 1/2 bound of Remark 1 (for l > 1000), which the paper does not prove either. Written by Claude Opus 5.5 (Anthropic), recompiled from scratch before publication. Code, verification command and line-by-line comparison with the paper: hh1997/ (36d5136). Zenodo archive (software): DOI 10.5281/zenodo.23498096. Errata note common to both papers (Zenodo, 2026-10-21, DOI 10.5281/zenodo.23535498): 9 points for this paper, each checked by a Lean theorem or by a script. None of them invalidates a theorem that we formalised. The list is not exhaustive.

Pour auditer : le README du dossier, section « How to check » (release v1.5) : énoncés figés, commande de revérification depuis un clone neuf, rapports d'axiomes enregistrés et écarts avec l'article. hh1997/README.md

To audit: the folder's README, section "How to check" (release v1.5): frozen statements, re-check command from a fresh clone, recorded axiom reports and differences from the paper. hh1997/README.md

Collaboration ouverte avec Benjamin Macindoe — « One obstruction, three faces »

Open collaboration with Benjamin Macindoe — "One obstruction, three faces"

Collaboration ouverte avec Benjamin Macindoe (chercheur indépendant), depuis juillet 2026. Le travail commun se fait dans un dépôt public, one-obstruction-three-faces : un registre des résultats (LEDGER.md), où chaque énoncé est vérifié indépendamment des deux côtés, et une note de travail commune (NOTE-v1, non publiée). Les échanges passent par des pull requests : huit ont été fusionnées, la dernière le 19 octobre 2026, et deux sont en cours de revue (rounds 19 et 20). Preprint de B. Macindoe : « Reduced coordinates for the Collatz map » (v3, DOI 10.5281/zenodo.21730505) ; voir aussi son papier miroir 3-adique. Entrée L-A1 du registre (récurrence de transport) : le résultat est classique (Halbeisen–Hungerbühler 1997, Lemme 9 ; Seifert 1988, Théorème 1 ; voir le changelog v0.10.1) ; la vérification Lean est côté Eric Merle, revérifiée sous Lean 4.34.0 (9934df4). Le détail des résultats communs sera publié ici avec son accord. Voir la page Cycles et le gateway interactif de B. Macindoe.

Open collaboration with Benjamin Macindoe (independent researcher), since July 2026. The joint work lives in a public repository, one-obstruction-three-faces: a ledger of results (LEDGER.md), where each statement is checked independently on both sides, and a joint working note (NOTE-v1, unpublished). Exchanges go through pull requests: eight have been merged, the last on 19 October 2026, and two are under review (rounds 19 and 20). B. Macindoe's preprint: "Reduced coordinates for the Collatz map" (v3, DOI 10.5281/zenodo.21730505); see also his 3-adic mirror paper. Ledger entry L-A1 (transport recurrence): the result is classical (Halbeisen–Hungerbühler 1997, Lemma 9; Seifert 1988, Theorem 1; see the changelog v0.10.1); the Lean check is on Eric Merle's side, re-checked on Lean 4.34.0 (9934df4). The detail of the joint results will be published here with his agreement. See the Cycles page and B. Macindoe's interactive gateway.

δ10 — Barina-Replacement Impossibility (Phase 64) — retiré (cartographie dépassée)

δ10 — Barina-Replacement Impossibility (Phase 64) — withdrawn (outdated cartography)

Lemme cartographique sur un catalogue fini de quatre sources (Salikhov 2007, Wu 2003, Rhin 1987, Simons–de Weger 2005), audité au 30/04/2026 : Lean vérifie la conclusion à partir de profils saisis à la main, pas les profils eux-mêmes. Retiré le 21/10/2026 (cartographie dépassée) : ne plus le citer comme un résultat. Revus contre les sources disponibles (notices zbMATH ; Rhin 1987 ; Simons–de Weger 2005), deux profils sont faux et un n'est pas vérifiable : Salikhov 2007 minore bien une forme linéaire en 1, ln 2 et ln 3, mais seulement au-delà d'une hauteur non explicite (notice zbMATH Zbl 1169.11032) ; Rhin 1987 en donne une minoration effective (Proposition p. 160, appliquée par Simons et de Weger), et pas seulement une mesure d'irrationalité de log 3 ; le chiffre attribué à Wu 2003 (7,6155) n'a pas pu être vérifié (sa notice zbMATH, Zbl 1099.11037, ne donne aucun exposant, et nous n'avons pas lu l'article). Ses trois conditions pour « remplacer BarinaVerification » (prédicat CanReplaceBarina du fichier Lean) sont : (1) donner une borne sur la forme linéaire S log 2 − k log 3 ; (2) être obtenue sans borne de vérification X₀ ; (3) impliquer n < 2⁷¹ pour tout cycle avec k ≤ 1322. Les conditions (1) et (3) décrivent en fait un remplacement de BakerSeparation dans la chaîne k ≤ 1322 (la (3) suppose encore la vérification de Bařina) ; or BakerSeparation n'est pas nécessaire pour ce résultat : Hercher 2023, avec la même vérification, l'implique déjà (erratum de la version Zenodo v4, item 4). Vérifié sous Lean 4.27.0, non revérifié depuis. → Voir branche study/delta10

Cartographic lemma on a finite catalogue of four sources (Salikhov 2007, Wu 2003, Rhin 1987, Simons–de Weger 2005), audited as of 2026-04-30: Lean checks the conclusion from hand-entered profiles, not the profiles themselves. Withdrawn on 2026-10-21 (outdated cartography): no longer to be cited as a result. Reviewed against the available sources (zbMATH reviews; Rhin 1987; Simons–de Weger 2005), two profiles are wrong and one cannot be checked: Salikhov 2007 does bound a linear form in 1, ln 2 and ln 3, but only beyond an unspecified height (zbMATH review Zbl 1169.11032); Rhin 1987 gives an effective lower bound for such a form (Proposition p. 160, applied by Simons and de Weger), not only an irrationality measure of log 3; the figure attributed to Wu 2003 (7.6155) could not be checked (its zbMATH entry, Zbl 1099.11037, gives no exponent, and we have not read the paper). Its three conditions for "replacing BarinaVerification" (predicate CanReplaceBarina of the Lean file) are: (1) give a bound on the linear form S log 2 − k log 3; (2) be derived without a verification bound X₀; (3) imply n < 2⁷¹ for every cycle with k ≤ 1322. Conditions (1) and (3) in fact describe a replacement of BakerSeparation in the k ≤ 1322 chain ((3) still requires Bařina's verification); but BakerSeparation is not needed for that result: Hercher 2023, with the same verification, already implies it (erratum of the Zenodo v4 version, item 4). Checked on Lean 4.27.0, not re-checked since. → See study/delta10 branch

Bibliothèque prototype : minima locaux et blocs (Lean 4) — archivée

Prototype library: local minima and blocks (Lean 4) — archived

Prototypes Lean 4 d'avril 2026 (environ 1 300 lignes, BlockDecomposition et BlockAmplification) sur les minima locaux d'un cycle, l'amplification de blocs et un découpage par moyenne géométrique (R73 / R76b). Malgré l'ancien titre « Décomposition Eliahou-Steiner en Lean 4 », ils ne formalisent pas Eliahou (1993) : la borne d'Eliahou reprise par Halbeisen et Hungerbühler (Théorème 2) est démontrée dans hh1997/, et une formalisation d'Eliahou 1993 par un tiers, non auditée par nous, est inscrite sur ccchallenge. BlockDecomposition déclare un axiome, hercher_m_le_91_axiom (au plus 91 minima locaux), qui inverse l'énoncé de Hercher 2023 (aucun m-cycle pour m ≤ 91) ; aucun théorème ne l'utilise. Archivée le 27/10/2026 : la bibliothèque ne sert à aucune des formalisations prévues par le labo, et nous ne lui connaissons aucune revérification sous Lean 4.34 (elle a été écrite pour Lean 4.27.0). Le code reste consultable pour l'historique.

April 2026 Lean 4 prototypes (about 1,300 lines, BlockDecomposition and BlockAmplification) on the local minima of a cycle, block amplification and a geometric-mean splitting (R73 / R76b). Despite the former title "Eliahou-Steiner block decomposition in Lean 4", they do not formalise Eliahou (1993): Eliahou's bound as restated by Halbeisen and Hungerbühler (Theorem 2) is proved in hh1997/, and a third-party formalisation of Eliahou 1993, not audited by us, is listed on ccchallenge. BlockDecomposition declares an axiom, hercher_m_le_91_axiom (at most 91 local minima), which reverses Hercher's 2023 statement (no m-cycle with m ≤ 91); no theorem uses it. Archived on 2026-10-27: the library serves none of the formalisations planned by the lab, and we know of no re-check of it under Lean 4.34 (it was written for Lean 4.27.0). The code remains available for the record.

δ11 — insuffisance conditionnelle (Salikhov 2007) — retiré

δ11 — conditional insufficiency (Salikhov 2007) — withdrawn

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 : ℝ, 0 < C_Salikhov et C_Salikhov < 10^{-30}, ce dernier non extrait de l'article) et repose sur une transposition de Salikhov 2007 (mesure d'irrationalité de ln 3 : $\mu(\ln 3) \leq 5{,}125$, DOI 10.1134/S1064562407060361) au problème ; cette transposition ne tient pas. Vérifié sous Lean 4.27.0, non revérifié depuis. Pour mémoire : Wu & Wang 2014 (J. Number Theory 142, 264-273, DOI 10.1016/j.jnt.2014.03.007) donnent $\mu(\log 3) < 5{,}117$. Cf. mea culpa #29 / #30 / #31 / #32. Branche study/E1-salikhov-2007-impossibility.

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 : ℝ, 0 < C_Salikhov and C_Salikhov < 10^{-30}, the last one not extracted from the paper) and rests on a transposition of Salikhov 2007 (irrationality measure of ln 3: $\mu(\ln 3) \leq 5.125$, DOI 10.1134/S1064562407060361) to the problem; that transposition does not hold. Checked on Lean 4.27.0, not re-checked since. For the record: Wu & Wang 2014 (J. Number Theory 142, 264-273, DOI 10.1016/j.jnt.2014.03.007) give $\mu(\log 3) < 5.117$. See mea culpa #29 / #30 / #31 / #32. Branch study/E1-salikhov-2007-impossibility.

Knight 2026 — high cycles

Knight 2026 — high cycles

K. Knight, « Collatz high cycles do not exist », Discrete Mathematics 349(3), article 114812 (2026), DOI 10.1016/j.disc.2025.114812 ; prépublication HAL hal-04261183 (2023). Selon son résumé, l'article montre qu'aucun « high cycle » (pour une longueur et un nombre de termes impairs donnés, un cycle rationnel particulier) n'est formé d'entiers positifs (comme pour les circuits, sauf 1-2-1) ; ce résultat n'exclut pas les autres cycles. Lecture close le 21/10/2026, sans intégration à nos dépôts. Une formalisation Lean 4 d'un tiers (tcosmo/Knight2026_lean) est inscrite sur ccchallenge, statut « Being formalised » (API : formalising) au 20/10/2026 ; nous ne l'avons pas auditée.

K. Knight, "Collatz high cycles do not exist", Discrete Mathematics 349(3), article 114812 (2026), DOI 10.1016/j.disc.2025.114812; HAL preprint hal-04261183 (2023). According to its abstract, the paper shows that no "high cycle" (for a given length and number of odd terms, one particular rational cycle) consists of positive integers (as for circuits, except 1-2-1); this result does not exclude other cycles. Reading closed on 2026-10-21, with no integration into our repositories. A third-party Lean 4 formalisation (tcosmo/Knight2026_lean) is listed on ccchallenge, status "Being formalised" (API: formalising) as of 2026-10-20; we have not audited it.