Pipeline éditorial
Editorial pipeline
Le projet est organisé autour d'un paper principal soumis (JAR Springer) et d'un portefeuille de cinq drafts Tier 1 + deux papers méta-méthodologiques. Ensemble : neuf publications ciblant la communauté de théorie des nombres, formal verification, et AI for Math.
The project is organized around one main submitted paper (JAR Springer) and a portfolio of five Tier 1 drafts + two meta-methodology papers. Together: nine publications targeting the number-theory, formal-verification, and AI-for-Math communities.
Paper 1 — JAR Springer (soumis)
Paper 1 — JAR Springer (submitted)
On the non-existence of non-trivial Collatz cycles: a conditional formal proof in Lean 4 with documented structural obstructions
28 pages. Preuve formelle conditionnelle modulo trois axiomes externes (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Profil d'axiomes minimal (3 axiomes Lean kernel : propext, Classical.choice, Quot.sound).
Architecture en 7 théorèmes centraux + auxiliaires, kernel-checked, reproductible via reproduce.sh.
28 pages. Conditional formal proof modulo three external axioms (BakerSeparation, BarinaVerification, DerivedLargeKBound).
Minimal axiom profile (3 Lean kernel axioms: propext, Classical.choice, Quot.sound).
Architecture: 7 central theorems + auxiliaries, kernel-checked, reproducible via reproduce.sh.
Contribution principale : pas la non-existence inconditionnelle (irréalisable dans le cadre des outils 2026), mais la cartographie rigoureuse des obstructions structurelles qui rend la conditionnalité nécessaire, pas arbitraire.
Main contribution: not unconditional non-existence (unattainable with 2026 tools), but the rigorous mapping of structural obstructions that makes the conditionality necessary, not arbitrary.
Statut : SOUMIS — JAR submission v1.1, 2026-04-27
Théorème Lean : no_nontrivial_cycle_phase59 (Phase59ContinuedFractions.lean:236)
DOI : 10.5281/zenodo.19790406
PDF : collatz-conditional-proof.pdf
Sources : paper/v2/
Status: SUBMITTED — JAR submission v1.1, 2026-04-27
Lean theorem: no_nontrivial_cycle_phase59 (Phase59ContinuedFractions.lean:236)
DOI: 10.5281/zenodo.19790406
PDF: collatz-conditional-proof.pdf
Sources: paper/v2/
Profil d'axiomes du résultat principal
Axiom profile of the main result
Le théorème no_nontrivial_cycle_phase59 repose sur un profil d'axiomes minimal et explicite. Aucun sorryAx dans la chaîne critique.
The theorem no_nontrivial_cycle_phase59 rests on a minimal, explicit axiom profile. No sorryAx in the critical chain.
| Catégorie | Identifiant Lean | Énoncé | Source |
|---|---|---|---|
| Axiomes Lean kernel (universels — toutes preuves Mathlib) | |||
| Kernel | propext |
Extensionnalité propositionnelle | Lean core |
| Kernel | Classical.choice |
Axiome du choix | Lean core |
| Kernel | Quot.sound |
Soundness des quotients | Lean core |
| Hypothèses externes documentées (les 3 conditions) | |||
| Externe 1 | BakerSeparation |
$|S \log 2 - k \log 3| > C/k^7$ effective | Laurent-Mignotte-Nesterenko 1995, JNT 55 |
| Externe 2 | BarinaVerification |
Tous $n < 2^{71}$ atteignent 1 | Barina 2025, J. Supercomp. 81, 810 |
| Externe 3 | DerivedLargeKBound |
Cycles ont $m \leq 91$ minima locaux | Hercher 2023, J. Integer Seq. 26.3.5 |
| Category | Lean identifier | Statement | Source |
|---|---|---|---|
| Lean kernel axioms (universal — every Mathlib proof) | |||
| Kernel | propext |
Propositional extensionality | Lean core |
| Kernel | Classical.choice |
Axiom of choice | Lean core |
| Kernel | Quot.sound |
Quotient soundness | Lean core |
| Documented external hypotheses (the 3 conditions) | |||
| External 1 | BakerSeparation |
$|S \log 2 - k \log 3| > C/k^7$ effective | Laurent-Mignotte-Nesterenko 1995, JNT 55 |
| External 2 | BarinaVerification |
All $n < 2^{71}$ reach 1 | Barina 2025, J. Supercomp. 81, 810 |
| External 3 | DerivedLargeKBound |
Cycles have $m \leq 91$ local minima | Hercher 2023, J. Integer Seq. 26.3.5 |
Lecture : si les trois conditions externes sont admises (deux hypothèses Diophantiennes + une vérification computationnelle Barina), alors la non-existence des cycles non-triviaux Collatz est prouvée formellement dans Lean 4, kernel-checked. Les axiomes kernel sont ceux que toute preuve Mathlib utilise — ils ne sont pas spécifiques à ce projet.
Reading: if the three external conditions are admitted (two Diophantine hypotheses + one computational Barina verification), then the non-existence of non-trivial Collatz cycles is formally proven in Lean 4, kernel-checked. The kernel axioms are those used by every Mathlib proof — they are not specific to this project.
Cinq drafts compacts en pipeline
Five compact drafts in pipeline
Multi-Brain Antifragile Pattern
Extended abstract 2 pages. Documentation du pattern multi-cerveau humain-IA antifragile, 13 mea culpa publics, triangulation 5-Agents, scaling 200× vs chercheur humain seul.
Extended abstract, 2 pages. Documents the antifragile human-AI multi-brain pattern, 13 public mea culpa, 5-agent triangulation, 200× scaling vs lone human researcher.
Cible : AITP 2026 (Aussois, août-septembre)
Effort restant : ~0.5 mois-personne (conversion LaTeX)
Statut : DRAFT v1
Target: AITP 2026 (Aussois, August-September)
Remaining effort: ~0.5 person-month (LaTeX conversion)
Status: DRAFT v1
Five Paradigms — Méta-théorème
Five Paradigms — Meta-theorem
10-15 pages. Taxonomie de cinq paradigmes pour la non-existence (Kolmogorov, Tao 2019, Fourier, Padé, recettes combinées) + méta-théorème de triangulation : la désaxiomatisation Baker pour Hercher gap est structurellement bloquée.
10-15 pages. Taxonomy of five paradigms for non-existence (Kolmogorov, Tao 2019, Fourier, Padé, combined recipes) + triangulation meta-theorem: the Baker deaxiomatization for the Hercher gap is structurally blocked.
Cible : Math. Intelligencer ou Notices AMS ou JNT expository
Effort restant : ~1-1.5 mois-personne
Statut : DRAFT v1
Target: Math. Intelligencer or Notices AMS or JNT expository
Remaining effort: ~1-1.5 person-months
Status: DRAFT v1
Eliahou-Steiner Block Decomposition Lean
12-18 pages. Première formalisation Lean 4 d'Eliahou-Steiner : 1301 LoC de library reusable (BlockDecomposition + BlockAmplification), IsLocalMin / IsLocalMax, cycleMinimaCount, R73 geometric mean splitting, R76b.
12-18 pages. First Lean 4 formalization of Eliahou-Steiner: 1301 LoC of reusable library (BlockDecomposition + BlockAmplification), IsLocalMin / IsLocalMax, cycleMinimaCount, R73 geometric mean splitting, R76b.
Cible : ITP 2026 (Lisbon, FLoC) ou CICM 2026 ou JAR
Effort restant : ~1.5-2 mois-personne
Statut : DRAFT v1
Target: ITP 2026 (Lisbon, FLoC) or CICM 2026 or JAR
Remaining effort: ~1.5-2 person-months
Status: DRAFT v1
Tautology Pitfalls — 13 Mea Culpa
8-12 pages. Typologie des pièges tautologiques en formalisation Diophantienne. Filtre 3-test (R72 / Steiner-Eliahou / Lagarias) avec sévérité 0-10. Trois case studies développés.
8-12 pages. Typology of tautological pitfalls in Diophantine formalization. 3-test filter (R72 / Steiner-Eliahou / Lagarias) with 0-10 severity. Three developed case studies.
Cible : JFR ou AITP 2026 ou AI for Math
Effort restant : ~1 mois-personne
Statut : DRAFT v1
Target: JFR or AITP 2026 or AI for Math
Remaining effort: ~1 person-month
Status: DRAFT v1
Universal Diophantine Arsenal — 72 Lean Theorems
14-20 pages. Catalogue complet des 72 théorèmes Lean développés post-JAR (R34-R96), organisés en 5 clusters : Steiner foundations, corrSum divisibility, modular universal, lacunary periodization, block decomposition.
14-20 pages. Complete catalog of the 72 Lean theorems developed post-JAR (R34-R96), organized in 5 clusters: Steiner foundations, corrSum divisibility, modular universal, lacunary periodization, block decomposition.
Cible : JNT ou Math. Comp. ou JAR
Effort restant : ~2-3 mois-personne (paper de référence, naming impeccable)
Statut : DRAFT v1 (Tier 2)
Target: JNT or Math. Comp. or JAR
Remaining effort: ~2-3 person-months (reference paper, impeccable naming)
Status: DRAFT v1 (Tier 2)
Ordre stratégique conseillé
Recommended strategic order
| Ordre | Paper | Effort | Probabilité d'acceptation | Justification |
|---|---|---|---|---|
| 1 | Paper 3 — AITP | 0.5 mois | ~75% | Deadline réelle août-sept ; format court ; méthodologie mature |
| 2 | Paper 6 — Méta-théorème | 1-1.5 mois | ~60% | Résultat phare (triangulation) ; risque de scoop si on attend |
| 3 | Paper 7 — Lean library | 1.5-2 mois | ~65% | Self-contained ; ITP/CICM 2026 ; library reusable au-delà Collatz |
| 4 | Paper 8 — Tautology pitfalls | 1 mois | ~55% | Soumettre après Paper 3 acceptation pour éviter overlap DOI |
| 5 | Paper 2 — Catalogue (Tier 2) | 2-3 mois | ~40% | Paper de référence ; peut être remplacé par repo public bien indexé |
| Order | Paper | Effort | Acceptance probability | Rationale |
|---|---|---|---|---|
| 1 | Paper 3 — AITP | 0.5 month | ~75% | Real deadline Aug-Sept; short format; mature methodology |
| 2 | Paper 6 — Meta-theorem | 1-1.5 months | ~60% | Flagship result (triangulation); scoop risk if delayed |
| 3 | Paper 7 — Lean library | 1.5-2 months | ~65% | Self-contained; ITP/CICM 2026; library reusable beyond Collatz |
| 4 | Paper 8 — Tautology pitfalls | 1 month | ~55% | Submit after Paper 3 acceptance to avoid DOI overlap |
| 5 | Paper 2 — Catalog (Tier 2) | 2-3 months | ~40% | Reference paper; could be replaced by a well-indexed public repo |
Total effort estimé : 6-9 mois-personne pour les 5 drafts ; 3 mois-personne pour le top-3 prioritaire.
Estimated total effort: 6-9 person-months for the 5 drafts; 3 person-months for the priority top-3.
Papers 4 et 5 — recherche en cours
Papers 4 and 5 — research in progress
Désaxiomatisation Baker partielle
Partial Baker deaxiomatization
Formalisation Lean de Salikhov 2007 ($\mu \leq 5.125$) ou Wu 2003 ($c = 5.117$) → théorème no_cycle_k_le_3732_unconditional. Réduction de 96% de la dépendance Baker (gap résiduel : $k \in [3733, 1.375 \cdot 10^{11}]$).
Lean formalization of Salikhov 2007 ($\mu \leq 5.125$) or Wu 2003 ($c = 5.117$) → theorem no_cycle_k_le_3732_unconditional. 96% reduction of Baker dependence (residual gap: $k \in [3733, 1.375 \cdot 10^{11}]$).
Effort estimé : ~13 mois-personne
Statut : PLAN
Estimated effort: ~13 person-months
Status: PLAN
Knight 2026 verified Lean
Conditional sur lecture du paper Knight 2026 ("Collatz high cycles do not exist", Discrete Math 349(3), 114812). Si méthode Sturmian/Christoffel inconditionnelle, formalisation Lean = nouveau résultat.
Conditional on reading the Knight 2026 paper ("Collatz high cycles do not exist", Discrete Math 349(3), 114812). If the Sturmian/Christoffel method is unconditional, Lean formalization = new result.
Effort : ?? (paywall Elsevier bloque l'évaluation)
Statut : EN ATTENTE
Effort: ?? (Elsevier paywall blocks evaluation)
Status: PENDING
Discussion communautaire
Community discussion
Discussions, questions, et propositions sur GitHub Discussions.
Discussions, questions, and proposals on GitHub Discussions.
→ Ouvrir / participer aux discussions → Open / join discussions