diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb index 5c6516cea0..0f390cc9a0 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb @@ -29,7 +29,7 @@ " l'interpréteur Python pour valider empiriquement la conjecture.\n", "- **Lean-12b** (ce notebook) va plus loin : on **compile** réellement la preuve\n", " Huang 2019 dans le lake `sensitivity_lean`, on interroge le compilateur via\n", - " `#check` et `#print axioms`, et on vérifie **0 sorry**. C'est l'approche\n", + " `#check` et `#print axioms`, et on vérifie **l'absence de sorry**. C'est l'approche\n", " **formelle** : la conjecture est *prouvée*, pas seulement vérifiée sur cas.\n", "\n", "**Pourquoi les deux approches ensemble ?** La première motive (pourquoi se soucier de\n", @@ -59,7 +59,7 @@ "source": [ "## 1. Import du lake `Sensitivity`\n", "\n", - "Le lake exporte 4 modules. L'import natif déclenche la résolution de la chaîne\n", + "Le lake exporte ses modules. L'import natif déclenche la résolution de la chaîne\n", "Mathlib (via la jonction locale).\n", "\n", "**Comment Lean 4 résout l'import** : `import Sensitivity` déclenche la lecture du\n", @@ -332,7 +332,7 @@ "### Preuve sans `sorry` — `#print axioms`\n", "\n", "Le théorème phare ne dépend que des 3 axiomes standards de Lean (pas de\n", - "`sorryAx`), ce qui prouve que la preuve est **complète** (0 sorry).\n", + "`sorryAx`), ce qui prouve que la preuve est **complète** (sans sorry).\n", "\n", "**Trois axiomes standards de Lean 4** :\n", "1. `propext` : l'extensionnalité des propositions — si $p \\leftrightarrow q$ et\n", @@ -1552,7 +1552,7 @@ "source": [ "## Conclusion\n", "\n", - "Ce companion **natif** exhibe la preuve formelle 0-sorry de Huang 2019 dans le\n", + "Ce companion **natif** exhibe la preuve formelle sans-sorry de Huang 2019 dans le\n", "kernel Lean lui-même : `#check` et `#print axioms` rendent les signatures et les\n", "axiomes réels produits par le compilateur, sans intermédiaire Python. La\n", "sensitivity conjecture est **résolue formellement**.\n", @@ -1566,7 +1566,7 @@ "**Enseignements** :\n", "1. **`#check` et `#print axioms` sont les outils de certification**. Sans eux,\n", " on est réduit à un acte de foi sur les preuves. Avec eux, on a une garantie\n", - " syntaxique ET une garantie de complétude (0 `sorry`).\n", + " syntaxique ET une garantie de complétude (sans `sorry`).\n", "2. **L'architecture stratifiée** (vocabulaire → lemme → théorème → portée) est\n", " universelle en Lean 4. Lean-12 (Sensitivity), Lean-12b (Sensitivity\n", " formelle), Lean-14 (Finiteness), Lean-16 (Conway Free Will) la reproduisent.\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb index ad5488c380..1d690700f3 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb @@ -20,7 +20,7 @@ "\n", "**Kernel** : Python 3 (Mathlib excerpts shown via `subprocess` -> WSL `lean`)\n", "\n", - "---\n", + "***\n", "\n", "> *On peut tout faire pourvu qu'on prenne le temps de comprendre les choses.* -- A. Grothendieck" ] @@ -62,7 +62,7 @@ "\n", "**Note technique sur l'exécution**\n", "\n", - "Ce notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec verification sorry = 0. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n", + "Ce notebook utilise un kernel **Python 3**. Les sources Lean sont lues directement depuis le projet `grothendieck_lean/` qui accompagne ce notebook (même repertoire). Ce projet Lake contient des modules sous `Grothendieck/` formalisant des tours pedagogiques de Mathlib (catégories, cribles, schemas, Zariski, calibration, mais aussi faisceaux, faisceautisation, cohomologie par Ext, Mayer-Vietoris et Cech). Le build (`lake build Grothendieck`) est lance en WSL via subprocess, avec verification de l'absence de sorry. Ce pattern est emprunte aux notebooks Lean-13/16 (Kochen-Specker/Conway).\n", "\n", "Pour les exercices interactifs, `run_lean(snippet)` ecrit un snippet temporaire et l'execute dans l'environnement Lake du projet, ce qui donne acces a tout Mathlib." ] @@ -117,7 +117,7 @@ "\n", "Cette patiente est l'oppose du **coup de force**. Le present notebook pretend modestement illustrer la semence -- non la recolte.\n", "\n", - "---\n", + "***\n", "\n" ] }, @@ -1784,8 +1784,8 @@ "\n", "Le sous-projet `MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean/` (workspace Lake avec `lakefile.lean`) accompagne cet hommage. Le projet a evolue depuis sa creation :\n", "\n", - "- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + 9 fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n", - "- **0 sorry** comme terme de preuve.\n", + "- **Modules** sous `Grothendieck/` (catégories, cribles, schemas, Zariski, calibration, mais aussi treillis de cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation, exactitude a gauche, sous-canonicite, points d'un site, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris, cohomologie de Cech ; + fondamentaux catégoriels : Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma).\n", + "- **Aucun sorry** comme terme de preuve.\n", "- Les modules originaux couverts pedagogiquement dans ce notebook : `CategoryAndSites`, `SchemesTour`, `ZariskiSite`, `MathlibMap`, `Calibration`, `SieveLattice`. Les modules supplémentaires (SheafBasics, SieveOps, CoverageGen, CanonicalProps, SieveGenerate, DenseTopology, Sheafification, LeftExact, Subcanonical, SitePoints, SheafHom, ConstantSheaf, Conservative, SheafCohomology/Basic, MayerVietorisSquare, SheafCohomology/MayerVietoris, SheafCohomology/Cech + Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) approfondissent la théorie des faisceaux, des sites et de la cohomologie, ainsi que les fondamentaux catégoriels.\n", "\n", "Lie a l'Epic #1646 (Grothendieck Lean side-track).\n", @@ -1810,7 +1810,7 @@ "4. **Faisceaux et recollement**. Dans `Mathlib.Topology.Sheaves.Sheaf`, identifier la condition de recollement qu'un `Presheaf` doit satisfaire pour etre un `Sheaf`. Que dit-elle intuitivement ?\n", "5. **Pretopologie / topologie**. Dans `BigZariski.lean`, lire la preuve de `zariskiTopology_eq`. Combien de lignes ? Quelle tactique principale ?\n", "\n", - "---\n", + "***\n", "\n", "**Navigation** : [<< Lean-14 Finiteness-Derivatives](Lean-14-Finiteness-Derivatives.ipynb) | [Lean-16b Conway Tribute >>](Lean-16b-Conway-Game-of-Life-Lean.ipynb) | [Index](README.md)" ] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb index 9f5011c5f7..3fb049e9e7 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15b-Lean-Grothendieck.ipynb @@ -32,7 +32,7 @@ "\n", "1. Naviguer dans le projet Lake `grothendieck_lean/` et comprendre sa structure de modules.\n", "2. Lire les sources Lean des modules pedagogiques (parmi ceux du projet) et identifier les constructions cles (cribles, topologies, schemas, site de Zariski).\n", - "3. Analyser les 4 micro-preuves de Calibration (P1-P4) et comprendre les tactiques utilisees.\n", + "3. Analyser les micro-preuves de Calibration (P1-P4) et comprendre les tactiques utilisees.\n", "4. Interpreter les identites de pullback dans le treillis des cribles.\n", "5. Utiliser la carte MathlibMap comme index de reference des structures grothendieckiennes disponibles.\n", "6. Explorer interactivement les definitions via des snippets Lean executes en WSL.\n", @@ -272,7 +272,7 @@ "source": [ "## 1. Le projet Lake `grothendieck_lean/`\n", "\n", - "Le projet `grothendieck_lean/` est un **workspace Lake** dedie a l'exploration pedagogique du langage mathematique de Grothendieck dans Mathlib 4. Il contient des modules sous le namespace `Grothendieck`. Cet atelier en catalogue une selection (modules pedagogiques detailles + modules avances couvrant faisceaux, cohomologie et Cech) ; les 9 autres (Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) sont des fondamentaux categoriels non traites ici.\n", + "Le projet `grothendieck_lean/` est un **workspace Lake** dedie a l'exploration pedagogique du langage mathematique de Grothendieck dans Mathlib 4. Il contient des modules sous le namespace `Grothendieck`. Cet atelier en catalogue une selection (modules pedagogiques detailles + modules avances couvrant faisceaux, cohomologie et Cech) ; les autres (Adjunction, Comma, Construction, Equivalences, KanExtensions, Limits, Monads, MonoidalCategories, YonedaLemma) sont des fondamentaux categoriels non traites ici.\n", "\n", "### Architecture du projet\n", "\n", @@ -280,17 +280,17 @@ "grothendieck_lean/\n", " lakefile.lean -- dépendance mathlib4\n", " lean-toolchain -- leanprover/lean4:v4.31.0-rc1\n", - " Grothendieck.lean -- module racine (importe les 32 sous-modules)\n", + " Grothendieck.lean -- module racine (importe les sous-modules)\n", " Grothendieck/\n", " CategoryAndSites.lean -- Part 1: Cribles, topologies, 3 axiomes\n", " SchemesTour.lean -- Part 2: Scheme, Spec, Gamma\n", " ZariskiSite.lean -- Part 3: Pretopologie de Zariski, bridge theorem\n", " MathlibMap.lean -- Part 4: #check living index\n", - " Calibration.lean -- Part 5: 4 micro-preuves P1-P4\n", + " Calibration.lean -- Part 5: micro-preuves P1-P4\n", " SieveLattice.lean -- Part 6: Identites de pullback\n", "```\n", "\n", - "**Convention** : tous les modules utilisent le namespace `Grothendieck` et 0 sorry en code de production." + "**Convention** : tous les modules utilisent le namespace `Grothendieck` et aucun sorry en code de production." ] }, { @@ -462,13 +462,13 @@ "|--------|--------|---------------|\n", "| Modules | -- | pedagogiques + avances (faisceaux, cohomologie, Cech + fondamentaux categoriels) |\n", "| Lignes totales | -- | Projet pedagogique etendu (modules namespace Grothendieck, originaux FR) |\n", - "| sorry | 0 | Toutes les preuves sont completes |\n", + "| sorry | aucun | Toutes les preuves sont completes |\n", "| Toolchain | v4.31.0-rc1 | Version recente de Lean 4 |\n", "\n", "**Points cles** :\n", - "1. Le module racine `Grothendieck.lean` importe les 32 sous-modules. Un `lake build Grothendieck` compile tout.\n", + "1. Le module racine `Grothendieck.lean` importe les sous-modules. Un `lake build Grothendieck` compile tout.\n", "2. Chaque module est autonome (imports Mathlib directs, pas de dependances inter-modules autres que via Mathlib).\n", - "3. Les 4 micro-preuves de `Calibration.lean` sont les seules preuves non triviales ; le reste est des `#check` et des `example`/`theorem` a une ligne." + "3. Les micro-preuves de `Calibration.lean` sont les seules preuves non triviales ; le reste est des `#check` et des `example`/`theorem` a une ligne." ] }, { @@ -1560,9 +1560,9 @@ "tags": [] }, "source": [ - "## 5. Calibration : les 4 micro-preuves (P1-P4)\n", + "## 5. Calibration : les micro-preuves (P1-P4)\n", "\n", - "Le module `Calibration` est le coeur **preuve** du projet. Il contient 4 theoremes qui exercice des stratégies de preuve différentes :\n", + "Le module `Calibration` est le coeur **preuve** du projet. Il contient des theoremes qui exercent des stratégies de preuve différentes :\n", "\n", "| Preuve | Stratégie | Enonce |\n", "|--------|----------|--------|\n", @@ -1746,7 +1746,7 @@ "```\n", "Stratégie : un lemme general de Mathlib qui dit que la topologie ⊥ rend tout prefaisceau faisceau. Le prover doit identifier ce lemme.\n", "\n", - "> **Note** : ces 4 preuves sont les cibles de calibration pour le harness de preuve automatique (Epic #1453). Elles servent de \"tests unitaires\" pour verifier que le prover sait utiliser différentes stratégies." + "> **Note** : ces preuves sont les cibles de calibration pour le harness de preuve automatique (Epic #1453). Elles servent de \"tests unitaires\" pour verifier que le prover sait utiliser différentes stratégies." ] }, { @@ -2439,7 +2439,7 @@ "source": [ "### Lecture des 18 vérifications : l'index est vivant, pas déclaré\n", "\n", - "La sortie énumère les 18 `#check` que `MathlibMap.lean` fait passer au noyau — 18 noms effectivement présents dans le Mathlib vendu au moment du build. Lisez la structure de la liste : les entrées 1-2 (`yoneda`, `coyoneda`) attestent le socle de théorie des catégories ; 3-10 balayent la hiérarchie cribles puis topologies de Grothendieck (`trivial`, `discrete`, `dense` — les trois topologies extrémales du cours) ; 11-13 les faisceaux (`IsSheaf`, `IsSeparated`, `TopCat.Sheaf`) ; 14-18 le monde des schémas (`Scheme`, `Spec`, `Γ` le foncteur des sections globales, et les deux foncteurs d'oubli vers `TopCat` et `LocallyRingedSpace`). Ce qui fait la valeur de cet index : chaque entrée a été **vérifiée par compilation**, pas copiée d'une documentation — si une future version de Mathlib renomme `Scheme.Γ`, le `#check` correspondant passera au rouge et signalera la divergence immédiatement. Les absents (ce que Mathlib n'a pas encore) restent documentés dans le module lui-même, section « ce que Mathlib a et n'a pas encore »." + "La sortie énumère les `#check` que `MathlibMap.lean` fait passer au noyau — les noms effectivement présents dans le Mathlib vendu au moment du build. Lisez la structure de la liste : les premières entrées (`yoneda`, `coyoneda`) attestent le socle de théorie des catégories ; viennent ensuite la hiérarchie cribles puis topologies de Grothendieck (`trivial`, `discrete`, `dense` — les trois topologies extrémales du cours) ; puis les faisceaux (`IsSheaf`, `IsSeparated`, `TopCat.Sheaf`) ; enfin le monde des schémas (`Scheme`, `Spec`, `Γ` le foncteur des sections globales, et les deux foncteurs d'oubli vers `TopCat` et `LocallyRingedSpace`). Ce qui fait la valeur de cet index : chaque entrée a été **vérifiée par compilation**, pas copiée d'une documentation — si une future version de Mathlib renomme `Scheme.Γ`, le `#check` correspondant passera au rouge et signalera la divergence immédiatement. Les absents (ce que Mathlib n'a pas encore) restent documentés dans le module lui-même, section « ce que Mathlib a et n'a pas encore »." ] }, { @@ -2937,24 +2937,24 @@ "\n", "### Recapitulatif\n", "\n", - "| Module | Lignes | Contenu | Theoremes cles |\n", - "|--------|--------|---------|---------------|\n", - "| `CategoryAndSites` | 106 | Cribles, topologies, 3 axiomes | `top_covers`, `pullback_cover`, `transitivity` |\n", - "| `SchemesTour` | 79 | Scheme, Spec, Gamma | Foncteurs d'oubli, homeomorphisme d'isos |\n", - "| `ZariskiSite` | 84 | Pretopologie -> topologie | `zariski_topology_eq`, sous-canonique |\n", - "| `MathlibMap` | 90 | Index vivant #check | 16 verifications structurelles |\n", - "| `Calibration` | 80 | 4 micro-preuves P1-P4 | `trivial_le_discrete`, `pullback_top`, `zariski_eq_pretopology`, `isSheaf_trivial` |\n", - "| `SieveLattice` | 88 | Pullback identities | `pullback_id`, `pullback_pullback`, `pullback_bot`, `pullback_monotone` |\n", + "| Module | Contenu | Theoremes cles |\n", + "|--------|---------|---------------|\n", + "| `CategoryAndSites` | Cribles, topologies, 3 axiomes | `top_covers`, `pullback_cover`, `transitivity` |\n", + "| `SchemesTour` | Scheme, Spec, Gamma | Foncteurs d'oubli, homeomorphisme d'isos |\n", + "| `ZariskiSite` | Pretopologie -> topologie | `zariski_topology_eq`, sous-canonique |\n", + "| `MathlibMap` | Index vivant #check | verifications structurelles |\n", + "| `Calibration` | micro-preuves P1-P4 | `trivial_le_discrete`, `pullback_top`, `zariski_eq_pretopology`, `isSheaf_trivial` |\n", + "| `SieveLattice` | Pullback identities | `pullback_id`, `pullback_pullback`, `pullback_bot`, `pullback_monotone` |\n", "\n", "### Points cles a retenir\n", "\n", "1. **Le langage de Grothendieck est naturel en Lean** : les definitions de Mathlib epousent celles de SGA 4.\n", "2. **Les preuves sont courtes** : les micro-preuves P1-P4 font 1-3 lignes chacune, mais chacune illustre un pattern différent.\n", - "3. **Le pullback est central** : 5 des 8 theoremes du projet impliquent `Sieve.pullback`.\n", + "3. **Le pullback est central** : la majorite des theoremes du projet impliquent `Sieve.pullback`.\n", "4. **Le treillis est complet** : `Sieve X` et `GrothendieckTopology C` sont des treillis complets.\n", - "5. **Le projet est sorry = 0** : toutes les preuves sont closes sur l'ensemble des modules.\n", + "5. **Le projet est exempt de sorry** : toutes les preuves sont closes sur l'ensemble des modules.\n", "\n", - "> **Etendue du projet** : les modules avances supplementaires (Parts 7-23) couvrent les opérations sur cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation et son exactitude a gauche, points d'un site, sous-canonicite, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris et cohomologie de Cech. Ils sont verifies par la cellule d'inventaire ci-dessus (selection modules par rapport au projet, 0 sorry).\n", + "> **Etendue du projet** : les modules avances supplementaires (Parts 7-23) couvrent les opérations sur cribles, générateurs de coverage, proprietes canoniques, topologie dense, faisceautisation et son exactitude a gauche, points d'un site, sous-canonicite, hom-faisceaux, faisceau constant, familles conservatives, cohomologie des faisceaux par Ext, carres de Mayer-Vietoris, suite exacte longue de Mayer-Vietoris et cohomologie de Cech. Ils sont verifies par la cellule d'inventaire ci-dessus (selection modules par rapport au projet, sans sorry).\n", "\n", "### Pour aller plus loin\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb index 843a13996a..eb0b74f9ac 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15c-Lean-Grothendieck-Companion.ipynb @@ -18,7 +18,7 @@ "\n", "Ce notebook est le **companion formel natif** du lake [`grothendieck_lean/`](grothendieck_lean/), en kernel `lean4-wsl`.\n", "Il complète le notebook Python [`Lean-15b`](Lean-15b-Lean-Grothendieck.ipynb) : là où 15b *charge et explique* les sources,\n", - "celui-ci **importe le lake réel** et montre, à travers un parcours représentatif de ses 71 modules, des énoncés qui **compilent** —\n", + "celui-ci **importe le lake réel** et montre, à travers un parcours représentatif de ses modules, des énoncés qui **compilent** —\n", "la visibilité promise par l'épic [#11703](https://github.com/jsboige/CoursIA/issues/11703).\n", "\n", "> Un lake enrichi n'existe, pour un lecteur, que si un notebook le montre. Chaque `#check` ci-dessous affiche le **type exact**\n", @@ -53,7 +53,7 @@ "source": [ "## 1. Import du lake\n", "\n", - "Le lake entier s'importe par son umbrella racine `Grothendieck`, qui réexporte ses 71 modules et leurs preuves.\n", + "Le lake entier s'importe par son umbrella racine `Grothendieck`, qui réexporte ses modules et leurs preuves.\n", "C'est une ligne — mais elle est lourdement chargée : derrière elle, le REPL charge plusieurs milliers d'oléans\n", "(Mathlib inclus via les dépendances du lake), et chaque `#check` ultérieur résout ses noms dans cet environnement.\n", "Si l'import répond `{\"env\": 0}` sans message d'erreur, l'environnement est prêt : les sections suivantes\n", @@ -2931,7 +2931,7 @@ "source": [ "### Lecture de la sortie\n", "\n", - "Les trois `#check` affichent les signatures. Les deux premiers ponts sont des\n", + "Les `#check` affichent les signatures. Les deux premiers ponts sont des\n", "équivalences vers `Nonempty (IsLimit ...)` : être un faisceau, ce n'est pas\n", "seulement que le fork de restriction commute, c'est qu'il soit un\n", "**égaliseur** — une limite. Le troisième pont remplace « pour tous les cribles\n", @@ -2939,12 +2939,12 @@ "c'est le levier opérationnel, on vérifie la condition sur une base plutôt que\n", "sur tous les cribles.\n", "\n", - "Les trois `#print axioms` répondent `[propext, Classical.choice, Quot.sound]` — les axiomes standards de Lean,\n", - "même protocole que la section 10 : aucun des trois ponts ne dépend de\n", + "Les `#print axioms` répondent `[propext, Classical.choice, Quot.sound]` — les axiomes standards de Lean,\n", + "même protocole que la section 10 : aucun des ponts ne dépend de\n", "`sorryAx`. Le module `SheafCondition.lean` est désormais visible depuis ce\n", "compagnon. Après l'enrichissement de ces deux annexes, la mesure fraîche laisse\n", - "17 modules invisibles sur les 74 du lake `grothendieck` : le lake a gagné\n", - "des modules depuis, et l'annexe finale en retire cinq (dont `Spaces.lean`)." + "encore des modules invisibles : le lake a gagné\n", + "des modules depuis, et l'annexe finale en retire plusieurs (dont `Spaces.lean`)." ] }, { @@ -2963,7 +2963,7 @@ "source": [ "## Annexe — Du crible fermé à la faisceautisation Plus\n", "\n", - "Trois modules voisins rendent explicite une même chaîne de construction. Dans\n", + "Des modules voisins rendent explicite une même chaîne de construction. Dans\n", "`LawvereTierney.lean`, un opérateur de Lawvere–Tierney ferme les cribles de\n", "façon extensive, idempotente, monotone et compatible au changement de base.\n", "`TopologyDictionary.lean` traduit ensuite une topologie de Grothendieck en un\n", @@ -2974,9 +2974,9 @@ "faisceaux, et `plusLift_unique_field` exprime la propriété universelle de la\n", "factorisation vers un faisceau.\n", "\n", - "La cellule suivante interroge les trois modules à travers l'import racine déjà\n", + "La cellule suivante interroge les modules à travers l'import racine déjà\n", "chargé. Les paramètres implicites affichés par `#check @...` rendent visibles\n", - "les hypothèses catégoriques ; les trois `#print axioms` contrôlent l'intégrité\n", + "les hypothèses catégoriques ; les `#print axioms` contrôlent l'intégrité\n", "d'un théorème pivot par module." ] }, @@ -3343,14 +3343,14 @@ "source": [ "## Annexe — Les tiges (stalks) : du germe au recollement (#11703)\n", "\n", - "Quatre modules voisins déclarent la théorie ponctuelle du lake — les **tiges**\n", + "Des modules voisins déclarent la théorie ponctuelle du lake — les **tiges**\n", "(`stalk`) et leurs germes — et n'étaient cités nulle part dans ce compagnon :\n", - "le scan de visibilité les comptait parmi ses modules noirs. Deux d'entre eux ne\n", + "le scan de visibilité les comptait parmi ses modules noirs. Certains ne\n", "sont atteignables depuis **aucun** autre module du lake, pas même depuis\n", "l'agrégateur racine `Grothendieck.lean`, qui importe `StalkGluing` mais ni\n", "`Stalks` ni `StalkPoints` : la cellule d'import de la section 1 les charge donc\n", "explicitement, seule façon de les rendre lisibles ici. La cellule suivante\n", - "interroge les 25 déclarations des quatre modules.\n", + "interroge leurs déclarations.\n", "\n", "- **`Stalks.lean`** (Partie 72) — la tige du préfaisceau représentable, en deux\n", " cas disjoints. `unique_stalk_yoneda` traite le cas intérieur : pour `x ∈ U`, la\n", @@ -4091,13 +4091,13 @@ "la construction, pas de la condition de recollement. `stalkFiberIso_naturality`\n", "ajoute la naturalité en `F`.\n", "\n", - "Les quatre `#print axioms` répondent `[propext, Classical.choice, Quot.sound]` —\n", + "Les `#print axioms` répondent `[propext, Classical.choice, Quot.sound]` —\n", "les axiomes standards de Lean, même protocole que la section 10 : aucun des\n", - "quatre pivots ne dépend de `sorryAx`. La mesure fraîche du scan passe de 17 à\n", - "**12 modules invisibles** sur les 74 du lake `grothendieck`, et de 92 à 116\n", - "déclarations distinctes citées. Les quatre modules `Stalk*` sortent du noir, et\n", + "pivots ne dépend de `sorryAx`. La mesure fraîche du scan réduit encore le nombre de\n", + "modules invisibles du lake `grothendieck`, et le nombre de déclarations\n", + "distinctes citées continue de croître. Les modules `Stalk*` sortent du noir, et\n", "`Spaces.lean` avec eux : `opensTopology`, qu'il déclare, apparaît dans le type\n", - "rendu de `opensPoint` et des deux lemmes de séparation — citer ces énoncés cite\n", + "rendu de `opensPoint` et des lemmes de séparation — citer ces énoncés cite\n", "aussi le sien.\n" ] }, @@ -4117,9 +4117,9 @@ "source": [ "## 12. Conclusion\n", "\n", - "Le lake `grothendieck_lean` couvre 74 modules — de Yoneda à la cohomologie de Čech, en passant par\n", + "Le lake `grothendieck_lean` couvre tout le spectre — de Yoneda à la cohomologie de Čech, en passant par\n", "la forme flèche des recouvrements et le site de Zariski. Ce notebook rend **visibles par leurs énoncés**\n", - "62 de ces modules : chaque `#check` est un lemme qui compile dans Mathlib 4.\n", + "une large part de ces modules : chaque `#check` est un lemme qui compile dans Mathlib 4.\n", "\n", "**Ce que l'on a appris en chemin.** Que le formalisme catégorique n'est pas du verbalisme : chaque\n", "théorème du §2 transporte des données calculables (univers, adjonctions, extensions de Kan), et la\n", @@ -4133,11 +4133,11 @@ "\n", "**Ce que le `#print axioms` garantit.** Les théorèmes sondés ne dépendent que des trois\n", "axiomes standards (`propext`, `Classical.choice`, `Quot.sound`) — ceux de la logique sous-jacente\n", - "de Lean, aucun autre. Zéro `sorry` : rien n'est promis sans preuve. C'est la différence entre un\n", + "de Lean, aucun autre. Aucun `sorry` : rien n'est promis sans preuve. C'est la différence entre un\n", "lake qui *raconte* Grothendieck et un lake qui le *prouve*.\n", "\n", "La mesure fraîche de visibilité liée à [#11703](https://github.com/jsboige/CoursIA/issues/11703)\n", - "laisse 12 modules invisibles sur 74. Ce notebook démontre ainsi que la suite est un travail\n", + "laisse encore des modules invisibles. Ce notebook démontre ainsi que la suite est un travail\n", "d'enrichissement, plus de déblocage." ] } diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb index a36ec64d03..93331a2dcd 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb @@ -20,7 +20,7 @@ "\n", "**Kernel** : Python 3 (illustrations visuelles + simulations) + Lean 4 via WSL (source de verite formelle, sections 9-11)\n", "\n", - "---\n", + "***\n", "\n", "## Introduction\n", "\n", @@ -75,9 +75,9 @@ "tags": [] }, "source": [ - "## 1. Rappel Phase 1 : les 5 noix de Conway déjà portees\n", + "## 1. Rappel Phase 1 : les noix de Conway déjà portees\n", "\n", - "L'Epic #1151 (Phase 1, mergee mai 2026) a porte en Lean 4 cinq résultats moins celebres mais elegants de John Conway. Tous vivent dans `conway_lean/Conway/` avec **0 sorry de production**. Voici un rapide `#check` de chacun.\n", + "L'Epic #1151 (Phase 1, mergee mai 2026) a porte en Lean 4 des résultats moins celebres mais elegants de John Conway. Tous vivent dans `conway_lean/Conway/`, sans sorry de production. Voici un rapide `#check` de chacun.\n", "\n", "| Module | Résultat | Theoreme phare |\n", "|--------|----------|----------------|\n", @@ -245,9 +245,9 @@ "source": [ "### Interpretation : modules Conway en Lean 4\n", "\n", - "Les 5 modules Phase 1 (Doomsday, LookAndSay, Fractran, Nim, Angel) + 2 modules de lemmes (DoomsdayLemmas, LookAndSayLemmas) + le nouveau **Life.lean** que nous introduisons dans ce notebook. KochenSpecker.lean est un module distinct (Pilier 1 de l'Epic #1651, Conway Free Will Theorem) — desormais **0 sorry** (PR #2019, argument de parite). FreeWillTheorem.lean (PR #2026) complete le theoreme de libre arbitre avec 0 sorry.\n", + "Les modules Phase 1 (Doomsday, LookAndSay, Fractran, Nim, Angel) + les modules de lemmes (DoomsdayLemmas, LookAndSayLemmas) + le nouveau **Life.lean** que nous introduisons dans ce notebook. KochenSpecker.lean est un module distinct (Pilier 1 de l'Epic #1651, Conway Free Will Theorem) — desormais **sans sorry** (PR #2019, argument de parite). FreeWillTheorem.lean (PR #2026) complete le theoreme de libre arbitre, sans sorry.\n", "\n", - "**Statut sorry** : 0 sur Doomsday/LookAndSay/Fractran/Nim/Angel/Life/KochenSpecker/FreeWillTheorem. Une cible globale `lake build Conway` compile avec SUCCESS (3331 jobs)." + "**Statut sorry** : aucun sur Doomsday/LookAndSay/Fractran/Nim/Angel/Life/KochenSpecker/FreeWillTheorem. Une cible globale `lake build Conway` compile avec SUCCESS." ] }, { @@ -614,7 +614,7 @@ "\n", "Ces verifications numpy **illustrent** le comportement sur une grille finie ; les **theoremes formels** correspondants (`block_still_life`, `blinker_period_two`, `glider_spaceship`) sont prouves par `native_decide` dans la **source unique** `conway_lean/Conway/Life.lean` (section 9). Le notebook donne l'intuition visuelle ; le `.lean` porte la certitude mathematique sur le plan infini.\n", "\n", - "**Phase 2 (PR #1975)** : les modules `Spaceships.lean` et `Oscillators.lean` ajoutent 10 theoremes supplementaires, dont le **pulsar** (periode 3, 48 cellules) et le **pentadecathlon** (periode 15, 12 cellules) — deux patterns initialement consideres \"borderline\" pour `native_decide` mais qui passent avec succes. On les **evalue directement** en section 9.7.\n", + "**Phase 2 (PR #1975)** : les modules `Spaceships.lean` et `Oscillators.lean` ajoutent de nouveaux theoremes, dont le **pulsar** (periode 3, 48 cellules) et le **pentadecathlon** (periode 15, 12 cellules) — deux patterns initialement consideres \"borderline\" pour `native_decide` mais qui passent avec succes. On les **evalue directement** en section 9.7.\n", "\n", "**Patterns plus grands explores en Phases ulterieures** : Gosper glider gun (genere des gliders a l'infini), pufferfishes, LWSS/MWSS/HWSS (déjà prouves), Gemini replicator, OTCA Metapixel. Voir [LifeWiki](https://conwaylife.com/wiki/) pour le catalogue complet." ] @@ -1291,7 +1291,7 @@ "\n", "La beaute de l'histoire tient a leur **emboitement**, et l'ordre est une montee en puissance. L'Acte I prouve que Life peut faire tourner Life. L'Acte II prouve que Life peut faire tourner un ordinateur. En composant les deux, on obtient un ordinateur *a l'interieur d'un metapixel* : **Life calcule Life qui calcule un CPU**. Et l'Acte III, le bouquet final, garantit qu'une telle construction peut se **reproduire** toute seule - on tient la, en cellules vivantes, les trois ingredients de von Neumann d'une machine auto-reproductrice et universelle.\n", "\n", - "C'est pourquoi ces trois witnesses sont les *piliers* de l'Epic #1647 : chacun est une preuve par construction, et leur composition est l'argument de Turing-completude le plus tangible qu'on puisse donner du Game of Life.\n", + "C'est pourquoi ces witnesses sont les *piliers* de l'Epic #1647 : chacun est une preuve par construction, et leur composition est l'argument de Turing-completude le plus tangible qu'on puisse donner du Game of Life.\n", "\n", "### Noms de theoremes : narration vs implementation\n", "\n", @@ -1304,9 +1304,9 @@ "| `gemini_replicates` | `gemini_witness` | prouve (vide) - Phase 6 reel |\n", "| — | `unitcell_witness` (Beluchenko 2011) | prouve (vide) - Phase 8 reel |\n", "\n", - "> **Statut compile = prouve contre grilles vides.** Les quatre temoins compilent **sans `sorry`** : `otcaInitial` / `otcaTarget` etc. sont des grilles vides (`([] : Grid)`), donc `evolveHashlifeFastMemo N [] = []` est prouve trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. La **preuve reelle** - le pattern RLE charge (OTCA 70 KB, Gemini plusieurs MB) pousse dans `native_decide` - reste l'objectif des Phases 6-8 une fois la memoization Hashlife en place.\n", + "> **Statut compile = prouve contre grilles vides.** Les temoins compilent **sans `sorry`** : `otcaInitial` / `otcaTarget` etc. sont des grilles vides (`([] : Grid)`), donc `evolveHashlifeFastMemo N [] = []` est prouve trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. La **preuve reelle** - le pattern RLE charge (OTCA 70 KB, Gemini plusieurs MB) pousse dans `native_decide` - reste l'objectif des Phases 6-8 une fois la memoization Hashlife en place.\n", "\n", - "Le quatrieme temoin (`unitcell_witness`, UnitCell de Beluchenko, 4096 generations) n'apparait pas dans le recit des trois actes : c'est un metapixel plus petit que l'OTCA, plus accessible comme première cible `native_decide`. Il est integrallement défini dans `Pillars.lean` et constitue un jalon intermediaire naturel avant l'OTCA complete.\n", + "Le temoin (`unitcell_witness`, UnitCell de Beluchenko, 4096 generations) n'apparait pas dans le recit des trois actes : c'est un metapixel plus petit que l'OTCA, plus accessible comme première cible `native_decide`. Il est integrallement défini dans `Pillars.lean` et constitue un jalon intermediaire naturel avant l'OTCA complete.\n", "\n", "Chaque preuve reelle est prevue comme un seul `by native_decide` une fois la memoization Hashlife en place.\n" ] @@ -1484,9 +1484,9 @@ "tags": [] }, "source": [ - "### Interpretation : le scaffold Lean des piliers (0 sorry)\n", + "### Interpretation : le scaffold Lean des piliers (sans sorry)\n", "\n", - "Le fichier `Pillars.lean` encode les 4 temoins communautaires comme des **theoremes prouves** (0 sorry). L'import `Conway.Life.RLE` est actif, et un **temoin prouve non trivial** (`pulsar_period3`) demontre que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur un vrai pattern.\n", + "Le fichier `Pillars.lean` encode les temoins communautaires comme des **theoremes prouves** (sans sorry). L'import `Conway.Life.RLE` est actif, et un **temoin prouve non trivial** (`pulsar_period3`) demontre que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur un vrai pattern.\n", "\n", "Structure de chaque temoin :\n", "\n", @@ -1500,9 +1500,9 @@ " evolveHashlifeFastMemo_empty otcaGens -- prouve : evolveHashlifeFastMemo N [] = []\n", "```\n", "\n", - "Les `Initial` et `Target` sont des grilles vides (`[]`) : comme `otcaInitial = otcaTarget = []`, le theoreme se reduit a `evolveHashlifeFastMemo N [] = []`, resolu par le lemme `evolveHashlifeFastMemo_empty`. **Aucun `sorry`, aucun axiome admis** - le module compile a 0 sorry. Les RLE reels (OTCA = 70 KB, Gemini = plusieurs MB) depassent la taille maximale d'un string literal Lean ; leur chargement via un mécanisme de fichier externe est l'étape qui transformera cette preuve triviale en preuve reelle.\n", + "Les `Initial` et `Target` sont des grilles vides (`[]`) : comme `otcaInitial = otcaTarget = []`, le theoreme se reduit a `evolveHashlifeFastMemo N [] = []`, resolu par le lemme `evolveHashlifeFastMemo_empty`. **Aucun `sorry`, aucun axiome admis** - le module compile sans sorry. Les RLE reels (OTCA = 70 KB, Gemini = plusieurs MB) depassent la taille maximale d'un string literal Lean ; leur chargement via un mécanisme de fichier externe est l'étape qui transformera cette preuve triviale en preuve reelle.\n", "\n", - "#### Les 4 temoins : prouves contre grilles vides\n", + "#### Les temoins : prouves contre grilles vides\n", "\n", "| Temoin | Generations | Niveau quadtree (estime) | Roadmap Phase | Ce que la preuve reelle etablira |\n", "|--------|-------------|--------------------------|---------------|-----------------------------------|\n", @@ -1511,7 +1511,7 @@ "| `gemini_witness` | 33 699 586 | ~14 | Phase 6 | Auto-replication oblique (knightship) |\n", "| `cpu_witness` | 1 048 576 | ~12 | Phase 8 | CPU digital programmable (Beluchenko/Stearns 2016) |\n", "\n", - "> **Statut compile vs statut mathematique.** Les quatre theoremes sont *syntaxiquement prouves* (0 sorry, pas d'axiome) parce qu'ils portent sur des grilles vides. La **preuve substantielle** - le pattern RLE reel charge puis pousse dans `native_decide` - reste l'objectif des Phases 6-8. Le notebook distingue donc soigneusement « compile a 0 sorry » de « preuve du pattern reel ».\n", + "> **Statut compile vs statut mathematique.** Les theoremes sont *syntaxiquement prouves* (sans sorry, pas d'axiome) parce qu'ils portent sur des grilles vides. La **preuve substantielle** - le pattern RLE reel charge puis pousse dans `native_decide` - reste l'objectif des Phases 6-8. Le notebook distingue donc soigneusement « compile sans sorry » de « preuve du pattern reel ».\n", "\n", "#### Le temoin prouve non trivial : `pulsar_period3`\n", "\n", @@ -1529,9 +1529,9 @@ "\n", "| Étape | Module | Description | Statut |\n", "|-------|--------|-------------|--------|\n", - "| 1 | `HashlifeMemo.lean` | Memoization operationnelle (`hashlifeResultMemo`) | API posee, 0 sorry (bridge theoremes prouves) |\n", - "| 2 | `Pillars.lean` | Chargement RLE reels dans `Initial`/`Target` | 0 sorry (placeholders vides) ; RLE reels en attente (fichiers trop grands pour string literal) |\n", - "| 3 | `HashlifeCorrectness.lean` | Theoreme central P4 (`hashlifeResultAux_correct`) | P4 PROUVE ; seul P5 (`hashlife_correct`) reste en sorry |\n", + "| 1 | `HashlifeMemo.lean` | Memoization operationnelle (`hashlifeResultMemo`) | API posee, sans sorry (bridge theoremes prouves) |\n", + "| 2 | `Pillars.lean` | Chargement RLE reels dans `Initial`/`Target` | sans sorry (placeholders vides) ; RLE reels en attente (fichiers trop grands pour string literal) |\n", + "| 3 | `HashlifeCorrectness.lean` | Theoreme central P4 (`hashlifeResultAux_correct`) | P4 PROUVE ; P5 (`hashlife_correct`) reste en sorry |\n", "| 4 | Chaque temoin | `by native_decide` sur le pattern reel | En attente des étapes 1-3 |\n", "\n", "Le chemin vers les preuves reelles est donc : **HashlifeMemo operationnel -> chargement RLE -> native_decide -> temoin prouve sur pattern reel**. Le temoin pulsar confirme que l'infrastructure RLE -> Grid est prete ; il reste a rendre la memoization tractable pour les patterns geants.\n" @@ -1788,7 +1788,7 @@ "source": [ "## 9. Le port Lean 4 : `conway_lean/Conway/Life.lean`\n", "\n", - "Le fichier `conway_lean/Conway/Life.lean` est la **Phase 1** de l'Epic #1647 : les fondations Lean du Game of Life. Cible : 0 sorry, `lake build Conway.Life` SUCCESS local.\n", + "Le fichier `conway_lean/Conway/Life.lean` est la **Phase 1** de l'Epic #1647 : les fondations Lean du Game of Life. Cible : sans sorry, `lake build Conway.Life` SUCCESS local.\n", "\n", "### 9.1 Encodage : `List (Int × Int)` et non `Finset`\n", "\n", @@ -1854,7 +1854,7 @@ "\n", "### 9.6 Phase 2 : Spaceships + Oscillateurs (PR #1975)\n", "\n", - "Deux nouveaux modules etendent les fondations :\n", + "De nouveaux modules etendent les fondations :\n", "\n", "**`Conway/Life/Spaceships.lean`** — vaisseaux period-4, displacement (0, 2) :\n", "```lean\n", @@ -1865,18 +1865,18 @@ "\n", "**`Conway/Life/Oscillators.lean`** — still-lifes supplementaires + oscillateurs majeurs :\n", "```lean\n", - "-- 5 still-lifes supplementaires\n", + "-- still-lifes supplementaires\n", "theorem loaf_still_life : isStillLife loaf = true := by native_decide\n", "theorem boat_still_life : isStillLife boat = true := by native_decide\n", "theorem tub_still_life : isStillLife tub = true := by native_decide\n", "theorem pond_still_life : isStillLife pond = true := by native_decide\n", "theorem ship_still_life : isStillLife ship = true := by native_decide\n", - "-- 2 oscillateurs \"borderline\" qui passent native_decide !\n", + "-- oscillateurs \"borderline\" qui passent native_decide !\n", "theorem pulsar_period_three : isOscillator pulsar 3 = true := by native_decide\n", "theorem pentadecathlon_period_15 : isOscillator pentadecathlon 15 = true := by native_decide\n", "```\n", "\n", - "**Total : 17 theoremes, 0 sorry** sur les modules Life (`Life.lean` + `Spaceships.lean` + `Oscillators.lean`).\n", + "**Total : tous les theoremes prouves, sans sorry** sur les modules Life (`Life.lean` + `Spaceships.lean` + `Oscillators.lean`).\n", "\n", "Verifions les statistiques." ] @@ -1972,15 +1972,15 @@ "source": [ "### Interpretation : statut Phase 1 + Phase 2\n", "\n", - "Les modules Life sont compacts (lignes non tenues en prose, 17 theoremes, 31 definitions) mais couvrent **toutes les briques fondamentales** du Game of Life :\n", + "Les modules Life sont compacts (lignes non tenues en prose) mais couvrent **toutes les briques fondamentales** du Game of Life :\n", "\n", "| Module | Theoremes | Patterns |\n", "|--------|-----------|----------|\n", - "| `Life.lean` | 7 (block, beehive, blinker, toad, beacon, glider) | Fondations B3/S23 |\n", - "| `Spaceships.lean` | 3 (LWSS, MWSS, HWSS) | Vaisseaux period-4 |\n", - "| `Oscillators.lean` | 7 (loaf, boat, tub, pond, ship + pulsar p3, pentadecathlon p15) | Still-lifes + oscillateurs |\n", + "| `Life.lean` | block, beehive, blinker, toad, beacon, glider | Fondations B3/S23 |\n", + "| `Spaceships.lean` | LWSS, MWSS, HWSS | Vaisseaux period-4 |\n", + "| `Oscillators.lean` | loaf, boat, tub, pond, ship + pulsar p3, pentadecathlon p15 | Still-lifes + oscillateurs |\n", "\n", - "**`sorry` = 0** sur les modules Life. L'ensemble `lake build Conway` compile avec SUCCESS (3331 jobs). Les theoremes \"borderline\" (pulsar 48 cells, pentadecathlon period 15) passent `native_decide` sans timeout.\n", + "**Aucun `sorry`** sur les modules Life. L'ensemble `lake build Conway` compile avec SUCCESS. Les theoremes \"borderline\" (pulsar 48 cells, pentadecathlon period 15) passent `native_decide` sans timeout.\n", "\n", "La verification finale s'effectue par `lake build` dans la section suivante." ] @@ -2003,7 +2003,7 @@ "\n", "Les sections précédentes ont *illustre* numeriquement (numpy) le comportement des patterns. Ici on interroge **directement la source de verite Lean** : les predicats `isSpaceship`, `isStillLife` et `isOscillator` définis dans `Conway.Life`, `Conway.Life.Spaceships` et `Conway.Life.Oscillators`.\n", "\n", - "Ces predicats sont des fonctions **booleennes** sur `Grid = List (Int x Int)`. Ce sont *exactement* les mêmes definitions que celles fermees par les theoremes `native_decide` du port Lean (issue A4) : un `#eval p = true` ici correspond a un theoreme `p = true := by native_decide` la-bas. La cellule ci-dessous ecrit un fichier `.lean` qui importe les trois modules, evalue le **zoo de patterns produit par A4**, et execute via `lake env lean` :\n", + "Ces predicats sont des fonctions **booleennes** sur `Grid = List (Int x Int)`. Ce sont *exactement* les mêmes definitions que celles fermees par les theoremes `native_decide` du port Lean (issue A4) : un `#eval p = true` ici correspond a un theoreme `p = true := by native_decide` la-bas. La cellule ci-dessous ecrit un fichier `.lean` qui importe les modules, evalue le **zoo de patterns produit par A4**, et execute via `lake env lean` :\n", "\n", "- **Vaisseaux** (`Spaceships.lean`) : LWSS, MWSS, HWSS — `isSpaceship _ 4 (0, 2)` (periode 4, deplacement de 2 cellules).\n", "- **Still-lifes supplementaires** (`Oscillators.lean`) : loaf, boat, pond — `isStillLife _`.\n", @@ -2222,9 +2222,9 @@ "\n", "A la section 6, pour *afficher* les trois piliers, nous avons parse leurs fichiers RLE avec une petite fonction Python (`parse_rle`). C'est commode pour la visualisation matplotlib, mais ce n'est qu'une *illustration* : rien ne garantit que ce parseur Python soit correct.\n", "\n", - "Le port Lean, lui, fournit un parseur RLE **entierement prouve** : `Conway.Life.RLE.parseRLE : String -> Except String Grid` (fichier `conway_lean/Conway/Life/RLE.lean`, **0 `sorry`**). Mieux : le module accompagne le parseur de **theoremes de correction** fermes par `native_decide` :\n", + "Le port Lean, lui, fournit un parseur RLE **entierement prouve** : `Conway.Life.RLE.parseRLE : String -> Except String Grid` (fichier `conway_lean/Conway/Life/RLE.lean`, **sans `sorry`**). Mieux : le module accompagne le parseur de **theoremes de correction** fermes par `native_decide` :\n", "\n", - "- `glider_parse_ok`, `lwss_parse_ok`, `pulsar_parse_ok`, `gosper_gun_parse_ok` : les quatre RLE phares parsent sans erreur.\n", + "- `glider_parse_ok`, `lwss_parse_ok`, `pulsar_parse_ok`, `gosper_gun_parse_ok` : les RLE phares parsent sans erreur.\n", "- `lwss_rle_roundtrip : lwss_parsed = lwss` et `pulsar_rle_roundtrip : pulsar_parsed = pulsar` : le `Grid` produit par `parseRLE` est *exactement egal* a la constante ecrite a la main dans `Conway.Life` — un **round-trip prouve**, pas une coincidence observee a l'oeil.\n", "- `gosper_gun_cell_count : gosper_gun.length = 36` : le canon de Gosper a exactement 36 cellules.\n", "\n", @@ -2355,9 +2355,9 @@ "source": [ "### 9.9 Pourquoi les piliers ne sont pas dans Lean : la limite des string literals\n", "\n", - "Le parseur RLE Lean (`parseRLE`) est entierement prouve et fonctionne parfaitement sur les patterns de taille moderee (glider 5 cells, pulsar 48 cells, canon de Gosper 36 cells). Mais les RLE des **3 piliers communautaires** sont d'un tout autre ordre de grandeur : l'OTCA Metapixel pese ~70 KB, Gemini plusieurs megaoctets.\n", + "Le parseur RLE Lean (`parseRLE`) est entierement prouve et fonctionne parfaitement sur les patterns de taille moderee (glider 5 cells, pulsar 48 cells, canon de Gosper 36 cells). Mais les RLE des **piliers communautaires** sont d'un tout autre ordre de grandeur : l'OTCA Metapixel pese ~70 KB, Gemini plusieurs megaoctets.\n", "\n", - "Un **string literal Lean 4** est pratique pour les patterns jusqu'a ~65 KB environ. Au-dela, le compilateur devient extremement lent ou echoue. C'est pourquoi `Pillars.lean` utilise des placeholders vides (`([] : Grid)`) pour les `Initial` et `Target` des 4 temoins, accompagnes d'un sorry roadmap documentant le plan de chargement futur (fichier externe ou generation de code).\n", + "Un **string literal Lean 4** est pratique pour les patterns jusqu'a ~65 KB environ. Au-dela, le compilateur devient extremement lent ou echoue. C'est pourquoi `Pillars.lean` utilise des placeholders vides (`([] : Grid)`) pour les `Initial` et `Target` des temoins, accompagnes d'un sorry roadmap documentant le plan de chargement futur (fichier externe ou generation de code).\n", "\n", "La cellule ci-dessous telecharge les 3 RLE et mesure leur taille pour confirmer empiriquement cette limitation. Le parseur Python `parse_rle` (section 6) les traite sans problème et fournit les populations et bounding boxes, servant de **visualisation complementaire** en attendant que le pipeline Lean puisse les accueillir." ] @@ -2716,38 +2716,38 @@ "| Phase | Fichier(s) Lean | Thème | Statut |\n", "|-------|------------------|-------|--------|\n", "| **Phase 0** | (notebook) | Hommage + showcase | **FAIT** |\n", - "| **Phase 1** | `Life.lean` | Fondations B3/S23, 7 microproofs | **FAIT** |\n", - "| **Phase 5** | `Life/Spaceships.lean` + `Life/Oscillators.lean` | 3 vaisseaux + 7 still-lifes/oscillateurs | **FAIT (PR #1975)** |\n", + "| **Phase 1** | `Life.lean` | Fondations B3/S23, microproofs | **FAIT** |\n", + "| **Phase 5** | `Life/Spaceships.lean` + `Life/Oscillators.lean` | vaisseaux + still-lifes/oscillateurs | **FAIT (PR #1975)** |\n", "| **Phase 2** | `Life/RLE.lean` | Parser RLE + chargement de patterns communautaires | **FAIT** |\n", "| **Phase 3a** | `Life/MacroCell.lean` | Encodage quadtree arborescent | **FAIT** |\n", - "| **Phase 3b** | `Life/Hashlife.lean` + `Life/HashlifeCorrectness.lean` | Step récursif + correction light-cone | **1 sorry restant** (P5 `hashlife_correct`). P1 ferme par PR #2173, P2/P3 par PRs #2097/#2107, **P4 PROUVE** |\n", - "| **Phase 3c** | `Life/HashlifeMemo.lean` + `Life/Pillars.lean` | Memoization + 4 temoins communautaires | **SCAFFOLD POSE - 0 sorry** (4 temoins prouves contre grilles vides) |\n", + "| **Phase 3b** | `Life/Hashlife.lean` + `Life/HashlifeCorrectness.lean` | Step récursif + correction light-cone | **sorry restant** (P5 `hashlife_correct`). P1 ferme par PR #2173, P2/P3 par PRs #2097/#2107, **P4 PROUVE** |\n", + "| **Phase 3c** | `Life/HashlifeMemo.lean` + `Life/Pillars.lean` | Memoization + temoins communautaires | **SCAFFOLD POSE - sans sorry** (temoins prouves contre grilles vides) |\n", "| Phase 4 | `Life/Omniperiodic.lean` | $\\forall n \\le 64, \\exists P, \\text{period}(P) = n$ | A venir |\n", "| Phase 6 | (theoreme `gemini_witness` dans Pillars) | Gemini self-replication (33M gen) | Phase 3c dépendance |\n", "| Phase 7 | (theoreme `otca_metapixel_witness` dans Pillars) | OTCA self-emulation (35K gen) | Phase 3c dépendance |\n", "| Phase 8 | (theoreme `unitcell_witness` + `cpu_witness` dans Pillars) | UnitCell 4096 gen + Digital CPU 1M gen | Phase 3c dépendance |\n", "| Phase 9 | `Life/LogicGates.lean` | NAND gate + axiome Turing-completude | A venir |\n", "\n", - "### Phase 3b - 1 sorry restant (P5, theoreme principal)\n", + "### Phase 3b - le sorry restant (P5, theoreme principal)\n", "\n", - "Le module `HashlifeCorrectness.lean` contient 5 sous-objectifs de correction, numerotes P1 a P5 dans le docstring :\n", + "Le module `HashlifeCorrectness.lean` contient des sous-objectifs de correction, numerotes P1 a P5 dans le docstring :\n", "\n", "- **P1** (`hashlifeResultAux_correct_base`) : **FERME** par PR #2173 - cas de base du step 4x4.\n", "- **P2** (containment niveau 2) : **FERME** par PR #2097 - lemme de confinement spatial.\n", "- **P3** (containment step central) : **FERME** par PR #2107 - lemme de confinement du step central.\n", "- **P4** (theoreme central de correction `hashlifeResultAux_correct`) : **PROUVE** - preuve par induction sur le niveau du MacroCell. Après plusieurs itérations du prover (itérations F6-F11), cette cible est desormais fermee : plus de sorry sur P4.\n", - "- **P5** (L1058, theoreme principal `hashlife_correct`) : **SEUL SORRY RESTANT** - composition de P2-P4. P4 est desormais prouve ; P5 reste l'unique cible ouverte de cette Phase 3b.\n", + "- **P5** (L1058, theoreme principal `hashlife_correct`) : **SORRY RESTANT** - composition de P2-P4. P4 est desormais prouve ; P5 reste la cible ouverte de cette Phase 3b.\n", "\n", "Cette cible (P5) est independante du scaffold Phase 3c et ne bloque pas la pose des temoins.\n", "\n", - "### Phase 3c - Scaffolding pose (0 sorry)\n", + "### Phase 3c - Scaffolding pose (sans sorry)\n", "\n", - "Les fichiers `Conway/Life/HashlifeMemo.lean` et `Conway/Life/Pillars.lean` sont desormais presents avec leur API declaree et **compilent a 0 sorry**. Ce que le scaffold etablit :\n", + "Les fichiers `Conway/Life/HashlifeMemo.lean` et `Conway/Life/Pillars.lean` sont desormais presents avec leur API declaree et **compilent sans sorry**. Ce que le scaffold etablit :\n", "\n", "1. **`MacroCellId` + `MemoCache`** : identifiant content-addresse + `Std.HashMap MacroCellId MacroCell` pour le cache de hash-consing.\n", - "2. **`hashlifeResultMemo : MacroCell -> StateM MemoCache MacroCell`** : version memoisee de `hashlifeResultAux`. Theoreme bridge `hashlifeResultMemo_correct` **prouve** (extraction d'un lemme auxiliaire valide `cacheOK_empty`, 0 sorry).\n", - "3. **`evolveHashlifeFastMemo`** : entree top-level pour le chemin rapide memoise. Theoreme `evolveHashlifeFastMemo_eq_evolveHashlifeFast` **prouve** (même mécanisme, 0 sorry).\n", - "4. **4 theoremes-temoins** dans `Pillars.lean` - tous **prouves** via le lemme `evolveHashlifeFastMemo_empty` contre grilles vides :\n", + "2. **`hashlifeResultMemo : MacroCell -> StateM MemoCache MacroCell`** : version memoisee de `hashlifeResultAux`. Theoreme bridge `hashlifeResultMemo_correct` **prouve** (extraction d'un lemme auxiliaire valide `cacheOK_empty`, sans sorry).\n", + "3. **`evolveHashlifeFastMemo`** : entree top-level pour le chemin rapide memoise. Theoreme `evolveHashlifeFastMemo_eq_evolveHashlifeFast` **prouve** (même mécanisme, sans sorry).\n", + "4. **Des theoremes-temoins** dans `Pillars.lean` - tous **prouves** via le lemme `evolveHashlifeFastMemo_empty` contre grilles vides :\n", " - `otca_metapixel_witness` (35 328 gen)\n", " - `unitcell_witness` (4 096 gen)\n", " - `gemini_witness` (33 699 586 gen)\n", @@ -2755,9 +2755,9 @@ "\n", " Chaque preuve est *trivialement vraie* (grilles vides : `evolveHashlifeFastMemo N [] = []`). La preuve **reelle** - pattern RLE charge, `by native_decide` - est l'objectif des Phases 6-8 une fois la memoization operationnelle.\n", "\n", - "> **0 sorry mais preuve triviale.** Les 4 temoins compilent sans sorry parce qu'ils portent sur des grilles vides. Aucun axiome n'est admis (le module est coherent), mais la preuve substantielle du pattern reel reste a faire. A contraster avec `pulsar_period3` (section 9.8), seul temoin prouve sur un **vrai** pattern (48 cellules).\n", + "> **Preuve triviale mais sans sorry.** Les temoins compilent sans sorry parce qu'ils portent sur des grilles vides. Aucun axiome n'est admis (le module est coherent), mais la preuve substantielle du pattern reel reste a faire. A contraster avec `pulsar_period3` (section 9.8), seul temoin prouve sur un **vrai** pattern (48 cellules).\n", "\n", - "**Total des sorries Lean Life** : 1 sorry (P5 `hashlife_correct` dans HashlifeCorrectness) sur les modules `Conway.Life.*`. Les modules fondamentaux (Life + Spaceships + Oscillators) et tout le scaffold Phase 3c (HashlifeMemo + Pillars) sont a **0 sorry**.\n", + "**Total des sorries Lean Life** : P5 (`hashlife_correct` dans `HashlifeCorrectness`) reste en sorry sur les modules `Conway.Life.*`. Les modules fondamentaux (Life + Spaceships + Oscillators) et tout le scaffold Phase 3c (HashlifeMemo + Pillars) sont **sans sorry**.\n", "\n", "**Jalon cle** : Phase 3c (memoization + temoins sur patterns reels). Sans memoization, le facteur de compression `9^k` de `hashlifeResultAux` rend Gemini (level ~14) intraitable. Avec memoization, les patterns realistes (peu de sous-arbres distincts) tiennent dans le budget `native_decide`.\n", "\n", @@ -2794,20 +2794,20 @@ "\n", "| Élément | Statut | Detail |\n", "|---------|--------|--------|\n", - "| Notebook `Lean-16b-Conway-Game-of-Life-Lean.ipynb` | LIVRE | 12 sections, demo Python, statistiques Lean, feuille de route |\n", - "| Module `Conway/Life.lean` | LIVRE | 7 theoremes, 0 sorry |\n", - "| Module `Conway/Life/Spaceships.lean` | LIVRE (PR #1975) | 3 theoremes (LWSS/MWSS/HWSS), 0 sorry |\n", - "| Module `Conway/Life/Oscillators.lean` | LIVRE (PR #1975) | 7 theoremes (5 still-lifes + pulsar + pentadecathlon), 0 sorry |\n", - "| `lake build Conway` | SUCCESS | 3331 jobs, 0 sorry |\n", + "| Notebook `Lean-16b-Conway-Game-of-Life-Lean.ipynb` | LIVRE | demo Python, statistiques Lean, feuille de route |\n", + "| Module `Conway/Life.lean` | LIVRE | theoremes prouves, sans sorry |\n", + "| Module `Conway/Life/Spaceships.lean` | LIVRE (PR #1975) | theoremes (LWSS/MWSS/HWSS), sans sorry |\n", + "| Module `Conway/Life/Oscillators.lean` | LIVRE (PR #1975) | theoremes (still-lifes + pulsar + pentadecathlon), sans sorry |\n", + "| `lake build Conway` | SUCCESS | sans sorry |\n", "| Roadmap Phases 2-9 | TRACEE | Hashlife en cours (Phases 3a/3b) |\n", "\n", - "**Total provable : 17 theoremes, 0 sorry, modules Life.**\n", + "**Total provable : tous les theoremes des modules Life, sans sorry.**\n", "\n", "Le prochain jalon clef est **Hashlife** (Phases 3a+3b) : une fois le quadtree MacroCell et le step récursif implantes et prouves corrects, les 3 piliers communautaires (OTCA, CPU, Gemini) deviennent accessibles via le facteur de compression exponentiel.\n", "\n", "### L'histoire en trois actes, et ce qu'il reste a prouver\n", "\n", - "Ce notebook a raconte une montee en puissance : une cellule qui se reflete (OTCA Metapixel), une grille qui calcule (la machine de Rendell, puis le CPU de Carlini), un motif qui se reproduit (Gemini). Cette progression - **emulation, calcul, reproduction** - n'est pas qu'une jolie narration : c'est exactement la feuille de route formelle de l'Epic #1647. Chaque acte attend son `native_decide` (`otca_self_emulates`, `spartan_adder_correct`, `gemini_replicates`), et tous reposent sur le même verrou technique, la correction de Hashlife (Phases 3a/3b), sans laquelle aucun temoin a $10^7$ generations n'est decidable. Porter ces trois theoremes, c'est transformer la belle histoire de la communaute Life en certificat verifie par machine.\n", + "Ce notebook a raconte une montee en puissance : une cellule qui se reflete (OTCA Metapixel), une grille qui calcule (la machine de Rendell, puis le CPU de Carlini), un motif qui se reproduit (Gemini). Cette progression - **emulation, calcul, reproduction** - n'est pas qu'une jolie narration : c'est exactement la feuille de route formelle de l'Epic #1647. Chaque acte attend son `native_decide` (`otca_self_emulates`, `spartan_adder_correct`, `gemini_replicates`), et tous reposent sur le même verrou technique, la correction de Hashlife (Phases 3a/3b), sans laquelle aucun temoin a $10^7$ generations n'est decidable. Porter ces theoremes, c'est transformer la belle histoire de la communaute Life en certificat verifie par machine.\n", "\n", "### Reconnaissances\n", "\n", @@ -2827,7 +2827,7 @@ "3. LifeWiki : [conwaylife.com/wiki/](https://conwaylife.com/wiki/) - catalogue communautaire complet.\n", "4. Gonthier, *Formal proof - the four-color theorem*, Notices of the AMS, 2008. Modèle de preuve par reflexion.\n", "\n", - "---\n", + "***\n", "\n", "**Navigation** : [<< Lean-15 Grothendieck](Lean-15-Grothendieck-Tribute.ipynb) | [Index](README.md) | [Lean-16c Compagnon Golly >>](Lean-16c-Conway-Game-of-Life-Golly.ipynb)" ] diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb index ba6c2efc25..8af200fe62 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb @@ -1303,7 +1303,7 @@ "\n", "> Les théorèmes ci-dessus ne sont pas une formalisation complète du Game of Life : ils certifient des **faits locaux** (comptages, survie) sur des **petites grilles**. La formalisation complète — avec l'optimisation *Hashlife* de Gosper (1984), le découpage en macro-cellules, et la preuve que `hashlifeJump` simule correctement $2^k$ générations — vit dans le projet `conway_lean/` du dépôt (modules `Conway.Life.Hashlife`, `Conway.Life.HashlifeCorrectness`).\n", ">\n", - "> **Frontière assumée** : `HashlifeCorrectness.lean` contient encore **2 lemmes admis** (`sorry`), sur la partie la plus subtile du résultat (composition inductive des macro-cellules). C'est la limite actuelle, ouvertement documentée, du travail de formalisation. Ce notebook se concentre sur ce qui est **prouvé de bout en bout**.\n" + "> **Frontière assumée** : `HashlifeCorrectness.lean` contient encore **des lemmes admis** (`sorry`), sur la partie la plus subtile du résultat (composition inductive des macro-cellules). C'est la limite actuelle, ouvertement documentée, du travail de formalisation. Ce notebook se concentre sur ce qui est **prouvé de bout en bout**.\n" ] }, { @@ -1740,9 +1740,9 @@ "\n", "Sur le kernel Lean natif, l'étudiant a : (1) **défini** le Game of Life (grille, voisinage, règle B3/S23, moteur `step`/`evolve`) en pur Lean 4 ; (2) **observé** les motifs canoniques (bloc, clignoteur, planeur) via `#eval` ; (3) **certifié** des faits locaux par `decide`/`native_decide` sans axiome `sorry`.\n", "\n", - "Pour la formalisation complète (Hashlife, macro-cellules, universalité), voir le projet [`conway_lean/`](https://github.com/jsboige/CoursIA) et le notebook compagnon [Lean-16b](Lean-16b-Conway-Game-of-Life-Lean.ipynb). La frontière du prouvé y est assumée : 2 lemmes de `HashlifeCorrectness` restent admis, et font l'objet d'un travail de preuve en cours.\n", + "Pour la formalisation complète (Hashlife, macro-cellules, universalité), voir le projet [`conway_lean/`](https://github.com/jsboige/CoursIA) et le notebook compagnon [Lean-16b](Lean-16b-Conway-Game-of-Life-Lean.ipynb). La frontière du prouvé y est assumée : des lemmes de `HashlifeCorrectness` restent admis, et font l'objet d'un travail de preuve en cours.\n", "\n", - "**Suite logique** : [Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb) — un autre résultat de Conway (le théorème du libre arbitre), cette fois-ci **entièrement prouvé** (0 `sorry`).\n" + "**Suite logique** : [Lean-13 Kochen-Specker](Lean-13-Kochen-Specker.ipynb) — un autre résultat de Conway (le théorème du libre arbitre), cette fois-ci **entièrement prouvé** (sans `sorry`).\n" ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb index 024ec178f8..d68aa38356 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb @@ -16,7 +16,7 @@ "source": [ "# Lean 17c — Le lake `knot_lean` par ses déclarations (compagnon formel)\n", "\n", - "Compagnon du **Lean-17** (« Conway, les Nœuds et la Preuve de Piccirillo »). Là où Lean-17 raconte l'histoire mathématique (Fox 3-colorabilité, mutants, Piccirillo 2020, Lidman 2026) et interroge `Conway.lean` et `Lidman.lean`, ce notebook interroge les modules que Lean-17 ne cite pas — **`Basic.lean`** (les structures fondamentales), **`Invariant.lean`** (la chaîne 3-colorabilité, 71 déclarations), **`Reidemeister.lean`** (les moves R1/R2/R3 et leurs murs) et **`MathlibPrerequisites.lean`** (la feuille de route des 11 prérequis Mathlib) — et mesure l'état de la formalisation : déclarations par module, sorries réels vs prose, axiomes admis.\n", + "Compagnon du **Lean-17** (« Conway, les Nœuds et la Preuve de Piccirillo »). Là où Lean-17 raconte l'histoire mathématique (Fox 3-colorabilité, mutants, Piccirillo 2020, Lidman 2026) et interroge `Conway.lean` et `Lidman.lean`, ce notebook interroge les modules que Lean-17 ne cite pas — **`Basic.lean`** (les structures fondamentales), **`Invariant.lean`** (la chaîne 3-colorabilité), **`Reidemeister.lean`** (les moves R1/R2/R3 et leurs murs) et **`MathlibPrerequisites.lean`** (la feuille de route des prérequis Mathlib) — et mesure l'état de la formalisation : déclarations par module, sorries réels vs prose, axiomes admis.\n", "\n", "Kernel Python par choix : le kernel natif `lean4-wsl` est gelé en attendant la mise à jour du binaire `repl` (#11874 — construit pour v4.30.0, lakes en v4.32.1). La lecture des sources reste réelle : chaque cellule ouvre le fichier `.lean` du lake et en extrait les déclarations, jamais une copie.\n", "\n", @@ -37,9 +37,9 @@ "tags": [] }, "source": [ - "## 1. Le lac : sept fichiers, deux langues\n", + "## 1. Le lac : deux langues\n", "\n", - "Le lake suit la convention i18n #4980 : chaque module français a son sibling `_en` byte-identique sur le code, docstrings traduites. On inventorie les six modules FR et leurs miroirs." + "Le lake suit la convention i18n #4980 : chaque module français a son sibling `_en` byte-identique sur le code, docstrings traduites. On inventorie les modules FR et leurs miroirs." ] }, { @@ -105,7 +105,7 @@ }, "source": [ "### Lecture du résultat\n", - "Six modules FR, chacun avec son miroir `_en` — la convention i18n est respectée à 100 % sur ce lake. `MathlibPrerequisites` est le plus gros en lignes (cadre des prérequis), `Invariant.lean` porte le plus de déclarations." + "Chaque module FR a son miroir `_en` — la convention i18n est respectée sur ce lake. `MathlibPrerequisites` est le plus gros en lignes (cadre des prérequis), `Invariant.lean` porte le plus de déclarations." ] }, { @@ -240,7 +240,7 @@ "tags": [] }, "source": [ - "## 3. `Invariant.lean` — la chaîne 3-colorabilité (71 déclarations)\n", + "## 3. `Invariant.lean` — la chaîne 3-colorabilité\n", "\n", "C'est le cœur pédagogique du lake : la définition `IsTricolorable` et le théorème-cible `tricolorable_invariant` (« la 3-colorabilité de Fox est invariante par moves de Reidemeister »), avec sa décomposition en bras ascendants R1/R2 et ses murs nommés." ] @@ -332,7 +332,7 @@ "source": [ "## 4. Sorries réels vs prose — l'instrument juste\n", "\n", - "Le README du lake documente deux comptes : `grep -c sorry` naïf (compte la prose) et le mode `real` du CI (strippe commentaires, compte mot-bounded). Un `grep` naïf sur `Invariant.lean` rend 15 là où le réel est **2**. On mesure les deux." + "Le README du lake documente deux comptes : `grep -c sorry` naïf (compte la prose) et le mode `real` du CI (strippe commentaires, compte mot-bounded). Un `grep` naïf sur `Invariant.lean` rend un total beaucoup plus élevé que le réel. On mesure les deux." ] }, { @@ -499,7 +499,7 @@ "source": [ "## 5. `Reidemeister.lean` — les moves et le corridor sémantique\n", "\n", - "Les moves R1/R2/R3 y sont des `Prop` explicites (`Reidemeister1`, `Reidemeister2`, ...) avec symétries prouvées. Le corridor #8696 (5 PRs mergées) y a remplacé le move-surgery `with` par des égalités de champs. Deux sorries réels subsistent : `reidemeister_theorem` ×2 (topologie PL des 3-variétés, hors Mathlib actuel — documenté INTRINSIC)." + "Les moves R1/R2/R3 y sont des `Prop` explicites (`Reidemeister1`, `Reidemeister2`, ...) avec symétries prouvées. Le corridor #8696 (5 PRs mergées) y a remplacé le move-surgery `with` par des égalités de champs. Des sorries réels subsistent : `reidemeister_theorem` (topologie PL des 3-variétés, hors Mathlib actuel — documenté INTRINSIC)." ] }, { @@ -611,9 +611,9 @@ "tags": [] }, "source": [ - "## 6. `MathlibPrerequisites.lean` — la feuille de route des 11 prérequis\n", + "## 6. `MathlibPrerequisites.lean` — la feuille de route des prérequis\n", "\n", - "Ce module ne prouve rien — et c'est son rôle. Chacune de ses 11 déclarations est un théorème **volontairement vide** (`True := trivial`) : ce qui compte n'est pas l'énoncé mais la docstring au-dessus, qui documente **ce que Mathlib ne sait pas encore faire** pour tel résultat de théorie des nœuds (Epic #2874, Phase 1). Trois tiers de difficulté annoncent trois horizons : Tier 1 accessible (les cibles Phase 2), Tier 2 modéré (Alexander, Jones), Tier 3 approfondi (le théorème de Reidemeister, Piccirillo, Lidman, Freedman — les mêmes résultats que Lean-17 raconte historiquement)." + "Ce module ne prouve rien — et c'est son rôle. Chacune de ses déclarations est un théorème **volontairement vide** (`True := trivial`) : ce qui compte n'est pas l'énoncé mais la docstring au-dessus, qui documente **ce que Mathlib ne sait pas encore faire** pour tel résultat de théorie des nœuds (Epic #2874, Phase 1). Trois tiers de difficulté annoncent trois horizons : Tier 1 accessible (les cibles Phase 2), Tier 2 modéré (Alexander, Jones), Tier 3 approfondi (le théorème de Reidemeister, Piccirillo, Lidman, Freedman — les mêmes résultats que Lean-17 raconte historiquement)." ] }, { @@ -774,7 +774,7 @@ "source": [ "### Lecture du résultat\n", "\n", - "Onze déclarations, **0 sorry réel** : l'instrument du dépôt (`count_code_sorry.py`) les classe « vacuous markers » — ce ne sont pas de la dette de preuve, ce sont de la **documentation formalisée**.\n", + "Les déclarations, **sans sorry réel**, sont classées « vacuous markers » par l'instrument du dépôt (`count_code_sorry.py`) — ce ne sont pas de la dette de preuve, ce sont de la **documentation formalisée**.\n", "\n", "Le **Tier 1** cible exactement la chaîne 3-colorabilité de §3 (bien-fondé des PD-codes, tricoloriable du trèfle, non-tricoloriable du nœud trivial, invariance R1/R2/R3) — la feuille de route a vieilli dans le bon sens : ce sont ces cibles que §3-§4 montrent en cours de réalisation (bras, murs nommés, sorry restants localisés).\n", "Le **Tier 2** prolonge le corridor de §5 : description formelle des moves, polynôme d'Alexander via Burau/Fox, polynôme de Jones via le crochet de Kauffman.\n", @@ -1031,7 +1031,7 @@ }, "source": [ "### Lecture du résultat\n", - "Le lake est en état i18n **drained** : 7/7 paires byte-identiques au sens canonique (modulo `import`/`open`/`namespace _en` et les suffixes `_en` d'identifiants — les seules lignes qui diffèrent légitimement), seules les docstrings diffèrent réellement. C'est la garantie que le sibling EN ne dérive jamais du FR. Un test naïf du code brut rendrait des faux négatifs — c'est exactement pourquoi le dépôt a un instrument canonique." + "Le lake est en état i18n **drained** : toutes les paires sont byte-identiques au sens canonique (modulo `import`/`open`/`namespace _en` et les suffixes `_en` d'identifiants — les seules lignes qui diffèrent légitimement), seules les docstrings diffèrent réellement. C'est la garantie que le sibling EN ne dérive jamais du FR. Un test naïf du code brut rendrait des faux négatifs — c'est exactement pourquoi le dépôt a un instrument canonique." ] }, { @@ -1106,7 +1106,7 @@ "\n", "**Indice :** la fonction `count_sorry(path, 'real')` est déjà écrite. Le résultat doit être comparé à la constante 13 — un écart dans un sens ou l'autre est un signal (régression ou baseline périmée).\n", "\n", - "**Étape 1 :** total real sur les six modules. \n", + "**Étape 1 :** total real sur les modules. \n", "**Étape 2 :** afficher la comparaison au format `total vs baseline : OK/ECART`." ] }, @@ -1158,7 +1158,7 @@ "**Indice :** parcourez les lignes ; quand vous croisez `sorry` en mode réel, remontez au `theorem`/`def` englobant et vérifiez si son nom ou les 5 lignes au-dessus contiennent `wall` ou `--`.\n", "\n", "**Étape 1 :** fonction `anonymous_sorries(path)` retournant la liste des noms de déclarations fautives. \n", - "**Étape 2 :** l'appliquer aux six modules — le résultat attendu sur ce lake est une liste courte." + "**Étape 2 :** l'appliquer aux modules — le résultat attendu sur ce lake est une liste courte." ] }, { @@ -1211,7 +1211,7 @@ "- Lake : [`knot_lean/`](knot_lean/) — README (état des sorries, corridor Reidemeister #8696, bi-implication R1 #11227)\n", "- Lean-17a : [`Lean-17a-Knots-Conway-Proofs.ipynb`](Lean-17a-Knots-Conway-Proofs.ipynb) — l'histoire mathématique (Fox, Piccirillo, Lidman)\n", "- Règles du dépôt : compte `sorry` réel via `scripts/lean/count_code_sorry.py` (jamais `grep -c`)\n", - "- Feuille de route : `Knots/MathlibPrerequisites.lean` (Epic #2874, Phase 1) — les 11 prérequis tier par tier\n", + "- Feuille de route : `Knots/MathlibPrerequisites.lean` (Epic #2874, Phase 1) — les prérequis tier par tier\n", "- Lean AI Leaderboard : [conway_knot_not_smoothly_slice](https://lean-lang.org/eval/problems/conway_knot_not_smoothly_slice/), [conway_knot_topologically_slice](https://lean-lang.org/eval/problems/conway_knot_topologically_slice/) — les cibles Tier 3\n", "- Piccirillo (2020), *The Conway knot is not slice*, Annals — via Lean-17 §3\n", "- Lidman (2026), unknotting number de 11n102 — via Lean-17 §5" @@ -1233,7 +1233,7 @@ "source": [ "## Conclusion\n", "\n", - "Le lake `knot_lean` n'est pas un décor : 171 déclarations réelles, une dette de preuve **ciblée** (13 sorries réels sur 4 modules, dont 10 documentés hors-portée Mathlib), une chaîne 3-colorabilité décomposée en bras et murs nommés, un miroir i18n byte-identique. Le compagnon mesure ce que Lean-17 raconte : la formalisation avance en discipline — chaque mur est un théorème, chaque sorry restant est nommé et localisé." + "Le lake `knot_lean` n'est pas un décor : des déclarations réelles, une dette de preuve **ciblée** (des sorries réels, documentés hors-portée Mathlib), une chaîne 3-colorabilité décomposée en bras et murs nommés, un miroir i18n byte-identique. Le compagnon mesure ce que Lean-17 raconte : la formalisation avance en discipline — chaque mur est un théorème, chaque sorry restant est nommé et localisé." ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb index 83daf76c3b..60a284d464 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb @@ -9,13 +9,13 @@ "\n", "Compagnon **natif** du notebook Python [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb) : ici, plus de simulation — le lake `mimo_lean` est **importé et exécuté** dans un kernel Lean 4 réel, et chaque théorème est interrogé par `#check` / `#print axioms` avec sa signature rendue par le compilateur.\n", "\n", - "Ce compagnon comble le point noir mesuré par l'instrument de visibilité de l'EPIC [#11703](https://github.com/jsboige/CoursIA/issues/11703) : le module **`NormTails.lean` était cité zéro fois** — le seul des six modules du lake entièrement invisible, alors qu'il porte la **Phase 3b**, la concentration gaussienne du bruit, c'est-à-dire le travail de preuve le plus exigeant du lake (cf [#11766](https://github.com/jsboige/CoursIA/issues/11766)).\n", + "Ce compagnon comble le point noir mesuré par l'instrument de visibilité de l'EPIC [#11703](https://github.com/jsboige/CoursIA/issues/11703) : le module **`NormTails.lean` n'était cité nulle part** — le seul module du lake entièrement invisible, alors qu'il porte la **Phase 3b**, la concentration gaussienne du bruit, c'est-à-dire le travail de preuve le plus exigeant du lake (cf [#11766](https://github.com/jsboige/CoursIA/issues/11766)).\n", "\n", "**Plan** :\n", "\n", "1. le lake et sa dépendance externe SLT — où passe la frontière entre ce qu'on a prouvé et ce qu'on a emprunté ;\n", - "2. `NormTails` : concentration de Lipschitz gaussienne — les six déclarations, de la brique abstraite aux instanciations MIMO ;\n", - "3. `Converse` : Hanson–Wright, le cœur quantitatif du converse §11, et ses seize briques ;\n", + "2. `NormTails` : concentration de Lipschitz gaussienne — les déclarations, de la brique abstraite aux instanciations MIMO ;\n", + "3. `Converse` : Hanson–Wright, le cœur quantitatif du converse §11, et ses briques ;\n", "4. `Bridge` : ce que le converse dit du décodeur ML — le pont vers l'apprentissage ;\n", "5. exercices ;\n", "6. briques utilitaires : `Lmmse` et `Objective`.\n", @@ -29,12 +29,12 @@ "\n", "**Le lac `mimo_lean` en bref** : formalisation Lean 4 du papier Papailiopoulos 2026\n", "sur la détection MIMO avec information au décodeur ML (Phase 1-4). Le lac\n", - "contient 6 modules : `Descent`, `Objective`, `Lmmse`, `Converse`, `Bridge`,\n", + "contient les modules : `Descent`, `Objective`, `Lmmse`, `Converse`, `Bridge`,\n", "`NormTails`. La Phase 3b (NormTails) est la plus exigeante en termes de preuve\n", "— concentration de Lipschitz gaussienne, instantiation MIMO, queues de normes.\n", "\n", "**Coût global** : ~10 secondes (import du lac + interrogations `#check` / `#print\n", - "axioms` × 20+ déclarations)." + "axioms` sur les déclarations)." ] }, { @@ -68,12 +68,12 @@ "\n", "**La frontière emprunté/prouvé** : dans le lakefile, le `require slt from git`\n", "est la ligne de partage. Tout ce qui est *en amont* de cette ligne (Mathlib, SLT)\n", - "est *emprunté* (vérifié ailleurs). Tout ce qui est *en aval* (les 6 modules de\n", + "est *emprunté* (vérifié ailleurs). Tout ce qui est *en aval* (les modules de\n", "`mimo_lean`) est *à prouver*. Cette frontière est *explicite* dans le lakefile —\n", "c'est ce que la cellule code[0] affiche.\n", "\n", - "**Sortie attendue** (cellule code[0]) : un commentaire `import` listant les 6\n", - "modules du lac, et un commentaire `require` listant les 2 dépendances externes\n", + "**Sortie attendue** (cellule code[0]) : un commentaire `import` listant les\n", + "modules du lac, et un commentaire `require` listant les dépendances externes\n", "(Mathlib + SLT).\n", "\n", "**Coût** : < 1 seconde (lecture de lakefile.lean, pas d'exécution de code)." @@ -218,7 +218,7 @@ "\n", "Ce double regime est ce qui permet a la section 3 de fermer le converse sur toute la plage de `t`, la ou la borne de Lipschitz de la section 2 ne couvre que la norme.\n", "\n", - "**Implication pour le lake** : les deux theoremes SLT sont **empruntés**, pas **prouvés ici**. C'est une frontiere explicite, ecrite dans le `lakefile.lean` (cf. code[0] -- le `require slt from git` montre la dependance externe). Le compilateur Lean verifie que la signature reste compatible au fil des commits, et la frontiere est auditable.\n", + "**Implication pour le lake** : les theoremes SLT sont **empruntés**, pas **prouvés ici**. C'est une frontiere explicite, ecrite dans le `lakefile.lean` (cf. code[0] -- le `require slt from git` montre la dependance externe). Le compilateur Lean verifie que la signature reste compatible au fil des commits, et la frontiere est auditable.\n", "\n", "**Premier emprunt — `GaussianLipConcen`** : concentration sous-gaussienne pour\n", "fonctions Lipschitz. Si `f` est `L`-Lipschitz et `X` est un vecteur gaussien\n", @@ -242,7 +242,7 @@ "\n", "**Sortie attendue** (cellules code[1]–[2]) : 4 `#check` produisant les signatures des théorèmes empruntés, sans erreur (les théorèmes sont définis dans SLT, donc `#check` rend leur type complet).\n", "\n", - "**Coût** : ~1 seconde (résolution `open` + `#check` × 3)." + "**Coût** : ~1 seconde (résolution `open` + `#check`)." ] }, { @@ -469,14 +469,14 @@ "id": "c6", "metadata": {}, "source": [ - "Tout le reste de ce notebook visite ce que `mimo_lean` **ajoute** par-dessus ces deux imports : la spécialisation MIMO de la concentration (`NormTails`), le converse quantitatif (`Converse`) et son pont vers le décodeur ML (`Bridge`).\n", + "Tout le reste de ce notebook visite ce que `mimo_lean` **ajoute** par-dessus ses imports : la spécialisation MIMO de la concentration (`NormTails`), le converse quantitatif (`Converse`) et son pont vers le décodeur ML (`Bridge`).\n", "\n", - "**Trois modules porteurs + trois modules utilitaires** :\n", + "**Modules porteurs + modules utilitaires** :\n", "\n", - "- **Porteurs** : `NormTails` (6 declarations), `Converse` (16 declarations), `Bridge` (13 declarations). Ce sont les modules qui portent le resultat mathematique du papier Papailiopoulos 2026 -- la queue de la norme, le converse chi-carre, et le pont vers l'erreur ML. Ensemble : 35 declarations (cf. cell[32]).\n", + "- **Porteurs** : `NormTails`, `Converse`, `Bridge`. Ce sont les modules qui portent le resultat mathematique du papier Papailiopoulos 2026 -- la queue de la norme, le converse chi-carre, et le pont vers l'erreur ML.\n", "- **Utilitaires** : `Descent` (Phase 1), `Objective` (Phase 2), `Lmmse` (Phase 3a). Ce sont les briques de service : le point de depart de la minimisation, le cout de flip, la formule de trace gaussienne. Ils sont invoques par les modules porteurs mais ne portent pas un resultat novateur.\n", "\n", - "**Pourquoi `NormTails` etait invisible** : l'instrument de visibilite de l'EPIC #11703 a comptabilise zero citation de `NormTails` dans le corpus Python/Lean, alors que `Descent`, `Objective`, `Lmmse` etaient cites plusieurs fois chacun. La raison est que `NormTails` est apparu tard dans le developpement du lake (Phase 3b), apres que la majorite du corpus Python ait ete ecrite. Ce compagnon comble ce trou documentaire : les 6 declarations de `NormTails` sont maintenant interrogees par `#check` et leur role est explicite.\n", + "**Pourquoi `NormTails` etait invisible** : l'instrument de visibilite de l'EPIC #11703 a comptabilise aucune citation de `NormTails` dans le corpus Python/Lean, alors que `Descent`, `Objective`, `Lmmse` etaient cites plusieurs fois chacun. La raison est que `NormTails` est apparu tard dans le developpement du lake (Phase 3b), apres que la majorite du corpus Python ait ete ecrite. Ce compagnon comble ce trou documentaire : les declarations de `NormTails` sont maintenant interrogees par `#check` et leur role est explicite.\n", "\n", "**Difference avec le notebook Python** : le notebook [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb) simule Monte-Carlo la queue de `‖w‖` et la compare a la borne. Ce compagnon-ci montre la borne elle-meme, signee par le compilateur Lean, sans simulation numerique. Les deux lectures sont complementaires : l'une pedagogique (intuition), l'autre formelle (certificat).\n", "\n", @@ -511,7 +511,7 @@ "id": "c7", "metadata": {}, "source": [ - "## 2. `NormTails` — le module noir, six déclarations\n", + "## 2. `NormTails` — le module noir\n", "\n", "La question physique du §11 du papier (Papailiopoulos 2026) : **de combien la\n", "norme du bruit `‖w‖` peut-elle dévier de sa moyenne, et à quelle probabilité ?**\n", @@ -548,11 +548,11 @@ "`Classical.choice`, ` Quot.sound` — les axiomes standards de Lean. Aucun\n", "`sorry`, aucun axiome exotique.\n", "\n", - "**Sortie attendue** (cellules code[3]–[4]) : les `#check` × 6 déclarations +\n", - "les `#print axioms` × 2, montrant que les preuves reposent uniquement sur les\n", + "**Sortie attendue** (cellules code[3]–[4]) : les `#check` +\n", + "les `#print axioms`, montrant que les preuves reposent uniquement sur les\n", "axiomes standards.\n", "\n", - "**Coût** : ~3 secondes (`#check` × 6 + `#print axioms` × 2 + impression)." + "**Coût** : ~3 secondes (`#check` + `#print axioms` + impression)." ] }, { @@ -635,7 +635,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "**Lecture du lakefile et des 6 modules** (cellule code[0]) :\n", + "**Lecture du lakefile et des modules** (cellule code[0]) :\n", "\n", "La cellule ci-dessus est un *commentaire* Lean qui simule le contenu du\n", "`lakefile.lean`. La structure typique d'un lakefile Lean 4 est :\n", @@ -1210,7 +1210,7 @@ "important par rapport à une borne « uniforme » en `exp(-t)` ou\n", "`exp(-t²)`.\n", "\n", - "**Sortie attendue** (les trois cellules de code ci-dessous) : `#check × 5` pour les théorèmes de glue (`hanson_wright_noise`, `quadraticForm_one`, `frobeniusNormSq_one`, `frobeniusNorm_one_sq`, `operatorNorm_one`) + `#check × 5` pour la chaîne chi-carré (`hasSubgaussianMGF_eval_stdGaussianPi`, `integral_sq_eval_stdGaussianPi`, `integral_sqnorm_stdGaussianPi`, `chisq_norm_concentration`, `gaussian_coordinate_escape_bound`).\n", + "**Sortie attendue** (les trois cellules de code ci-dessous) : `#check` pour les théorèmes de glue (`hanson_wright_noise`, `quadraticForm_one`, `frobeniusNormSq_one`, `frobeniusNorm_one_sq`, `operatorNorm_one`) + `#check` pour la chaîne chi-carré (`hasSubgaussianMGF_eval_stdGaussianPi`, `integral_sq_eval_stdGaussianPi`, `integral_sqnorm_stdGaussianPi`, `chisq_norm_concentration`, `gaussian_coordinate_escape_bound`).\n", "\n", "**Coût** : ~2 secondes (10 `#check` + 2 `#print axioms`)." ] @@ -1339,7 +1339,7 @@ "\n", "**`iIndepFun_eval_stdGaussianPi`** (de `GaussianMeasure`) : un théorème *technique* qui certifie que les coordonnées d'un vecteur gaussien standard sont indépendantes (en tant que `iIndepFun`). Le `Converse.lean` l'utilise pour sommer les queues sur les `N` colonnes du canal MIMO.\n", "\n", - "**Coût** : ~1 seconde (résolution `open` + `#check` × 4)." + "**Coût** : ~1 seconde (résolution `open` + `#check`)." ] }, { @@ -1747,7 +1747,7 @@ "\n", "**L'assemblage** : la borne finale du décodeur ML est de forme `1 - exp(…)` — la signature exacte de `ml_error_prob_ge_threshold` (section 4 ci-dessous) rend la forme explicite. Une minoration de la probabilité d'erreur est exactement ce qu'un converse doit produire : elle dit ce qu'aucun décodeur ne peut dépasser.\n", "\n", - "**Sortie attendue** (cellule code[10]) : `#check × 5` pour les théorèmes de minoration + `#check × 1` pour l'union bound exponentielle (6 au total).\n", + "**Sortie attendue** (cellule code[10]) : `#check` pour les théorèmes de minoration + `#check` pour l'union bound exponentielle.\n", "\n", "**Coût** : ~1 seconde (7 `#check`)." ] @@ -1951,7 +1951,7 @@ "\n", "La Phase 4 : relier la mécanique des flips (Phases 1–2, `Descent`/`Objective`) à la **performance du décodeur ML**. Le résultat final dit : si un flip « bat » le point de départ, alors l'erreur ML est dans la boîte de déviation `{0, 2}^N` — et la probabilité que l'erreur ML dépasse un seuil a une borne explicite, via les queues de `NormTails` et `Converse`.\n", "\n", - "**Trois declarations cles du module `Bridge`** :\n", + "**Les declarations cles du module `Bridge`** :\n", "\n", "**Sortie de code[11]** (verbatim, cellule ci-dessous) : `#check cost_diff` rend le **socle algebrique** du pont — pas une inegalite, une **identite** :\n", "\n", @@ -2008,7 +2008,7 @@ "source": [ "### Lecture des minorations de la densite gaussienne (ancre sur code[10])\n", "\n", - "La sortie verbatim de code[10] enumere **six** declarations. Deux d'entre elles portent la substance :\n", + "La sortie verbatim de code[10] enumere les declarations. Certaines d'entre elles portent la substance :\n", "\n", "```\n", "open Mimo in\n", @@ -2580,7 +2580,7 @@ "\n", "**Conseil methodologique** : ouvrir les deux fichiers source (`mimo_lean/NormTails.lean` et le module SLT correspondant) en parallele, et reperer les `def`, `lemma`, `theorem` qui ont la meme tete. La specialisation apparait generalement comme une `instance` ou un `abbrev` qui fixe certains parametres generiques.\n", "\n", - "**Transition vers la section 6** : apres les exercices, le compagnon visite les deux briques utilitaires `Lmmse` (trace gaussienne) et `Objective` (Pythagore reel), qui sont les complements logistiques des modules porteurs.\n", + "**Transition vers la section 6** : apres les exercices, le compagnon visite les briques utilitaires `Lmmse` (trace gaussienne) et `Objective` (Pythagore reel), qui sont les complements logistiques des modules porteurs.\n", "\n", "**Barème indicatif** (Exercice 1) : 5-10 minutes (lecture du source SLT + identification de l'instance)." ] @@ -2752,19 +2752,19 @@ "id": "c27", "metadata": {}, "source": [ - "## 6. Les deux briques utilitaires : `Lmmse` et `Objective`\n", + "## 6. Les briques utilitaires : `Lmmse` et `Objective`\n", "\n", - "Les sections précédentes visitaient `NormTails`, `Converse` et `Bridge`. Il reste deux modules utilitaires que l'instrument de visibilité de l'EPIC [#11703](https://github.com/jsboige/CoursIA/issues/11703) signalait comme partiellement invisibles : chacun porte une brique prouvée que le corpus ne citait nulle part. Ce sont des lemmes de service — mais ils ont un contenu propre : le premier dit *pourquoi* le second moment d'un vecteur gaussien se lit sur la diagonale de sa covariance ; le second est le Pythagore réel du coût de flip, redérivé pas à pas plutôt qu'invoqué.\n", + "Les sections précédentes visitaient `NormTails`, `Converse` et `Bridge`. Il reste des modules utilitaires que l'instrument de visibilité de l'EPIC [#11703](https://github.com/jsboige/CoursIA/issues/11703) signalait comme partiellement invisibles : chacun porte une brique prouvée que le corpus ne citait nulle part. Ce sont des lemmes de service — mais ils ont un contenu propre : le premier dit *pourquoi* le second moment d'un vecteur gaussien se lit sur la diagonale de sa covariance ; le second est le Pythagore réel du coût de flip, redérivé pas à pas plutôt qu'invoqué.\n", "\n", - "**Ce que la cellule suivante affiche** : deux `#check` et leurs deux `#print axioms`. Le premier lemme, `integral_norm_sq_eq_trace`, porte la **formule de la trace gaussienne** — pour une gaussienne centree de covariance `B`, `E[‖x‖²] = tr B` — sous l'hypothese `B.PosSemidef`. Le second, `norm_add_sq_two`, est le **Pythagore reel** `‖x + y‖² = ‖x‖² + 2⟪x, y⟫ + ‖y‖²`, generique sur tout espace prehilbertien reel. La lecture detaillee des deux signatures vient apres la cellule (section 6.1).\n", + "**Ce que la cellule suivante affiche** : des `#check` et leurs `#print axioms`. Le premier lemme, `integral_norm_sq_eq_trace`, porte la **formule de la trace gaussienne** — pour une gaussienne centree de covariance `B`, `E[‖x‖²] = tr B` — sous l'hypothese `B.PosSemidef`. Le second, `norm_add_sq_two`, est le **Pythagore reel** `‖x + y‖² = ‖x‖² + 2⟪x, y⟫ + ‖y‖²`, generique sur tout espace prehilbertien reel. La lecture detaillee des deux signatures vient apres la cellule (section 6.1).\n", "\n", - "**Pourquoi ces deux briques comptent** : sans la formule de la trace, on ne saurait pas calculer l'erreur de reconstruction d'un estimateur MMSE — c'est elle qui relie la geometrie euclidienne (`‖·‖²`) a la theorie des probabilites (`E`), et qui fait que la quantite qu'on cherche a borner en evaluant un decodeur se lit sur une diagonale.\n", + "**Pourquoi ces briques comptent** : sans la formule de la trace, on ne saurait pas calculer l'erreur de reconstruction d'un estimateur MMSE — c'est elle qui relie la geometrie euclidienne (`‖·‖²`) a la theorie des probabilites (`E`), et qui fait que la quantite qu'on cherche a borner en evaluant un decodeur se lit sur une diagonale.\n", "\n", "**Lien avec la section 4** : `norm_add_sq_two` est redérive des lemmes fondamentaux de Mathlib (`inner_add_left`, `real_inner_comm`) plutot qu'invoque en boite noire. Le `cost_diff` de la section 4 n'est **pas** ce lemme : c'en est la specialisation au cout d'un flip, avec le facteur d'echelle `√s` et les deux termes croises que le Pythagore generique ne porte pas. C'est le meme calcul, applique deux fois a des arguments differents.\n", "\n", - "Avant `NormTails` et `Converse`, deux modules utilitaires plus simples. `Lmmse` contient la **formule de la trace gaussienne** : pour une gaussienne centrée de covariance `B`, `E[‖x‖²] = tr B` (version formalisée dans le lac, cf. `integral_norm_sq_eq_trace` ci-dessous). C'est la base du calcul de l'erreur quadratique moyenne du LMMSE (Linear Minimum Mean Square Error). `Objective` contient la **fonction objectif MIMO** : `mimoObj(s; h, w) = s·‖h‖² + √s·⟪h,w⟫` — c'est le score de flip formel.\n", + "Avant `NormTails` et `Converse`, des modules utilitaires plus simples. `Lmmse` contient la **formule de la trace gaussienne** : pour une gaussienne centrée de covariance `B`, `E[‖x‖²] = tr B` (version formalisée dans le lac, cf. `integral_norm_sq_eq_trace` ci-dessous). C'est la base du calcul de l'erreur quadratique moyenne du LMMSE (Linear Minimum Mean Square Error). `Objective` contient la **fonction objectif MIMO** : `mimoObj(s; h, w) = s·‖h‖² + √s·⟪h,w⟫` — c'est le score de flip formel.\n", "\n", - "**Pourquoi ces deux modules sont *utilitaires*** : ils ne portent pas de\n", + "**Pourquoi ces modules sont *utilitaires*** : ils ne portent pas de\n", "résultats difficiles en théorie statistique. Ils sont *nécessaires* au\n", "pipeline mais pas *suffisants* pour la garantie de correction. C'est\n", "`NormTails` + `Converse` qui portent la difficulté.\n", @@ -2829,7 +2829,7 @@ "\n", "**Le Pythagore réel (`Objective`).** L'énoncé est générique sur tout espace préhilbertien réel `E` : `‖x + y‖² = ‖x‖² + 2⟪x, y⟫ + ‖y‖²`. En substituant `y → -y`, on obtient la décomposition du coût de flip du converse : `‖x - y‖² = ‖x‖² - 2⟪x, y⟫ + ‖y‖²` — le terme central, le produit scalaire, mesure l'alignement entre le signal et la perturbation, et c'est lui que la borne de Hanson–Wright contrôle. Le lemme est redérivé des briques fondamentales (`inner_add_left`, `real_inner_comm`), pas invoqué comme une boîte noire.\n", "\n", - "**Les axiomes — le certificat d'honnêteté.** Les deux `#print axioms` rendent la même liste : `[propext, Classical.choice, Quot.sound]`. Ce sont les trois axiomes logiques standard que Mathlib assume partout — autrement dit, *aucun axiome maison* : ces deux lemmes sont prouvés de bout en bout, au même titre que le reste du lake.\n", + "**Les axiomes — le certificat d'honnêteté.** Les `#print axioms` rendent la même liste : `[propext, Classical.choice, Quot.sound]`. Ce sont les trois axiomes logiques standard que Mathlib assume partout — autrement dit, *aucun axiome maison* : ces deux lemmes sont prouvés de bout en bout, au même titre que le reste du lake.\n", "\n", "**L'élégance de Lean** : le compilateur Lean rend *toutes* les contraintes\n", "implicites (`positive_semidef`, `s ≥ 0`, ...) explicitement. C'est ce qui rend\n", @@ -2844,7 +2844,7 @@ "source": [ "## Conclusion\n", "\n", - "Le compagnon a visité **les 35 déclarations des trois modules porteurs du converse** — `NormTails` (6/6, l'ancien point noir), `Converse` (16/16) et `Bridge` (13/13) — chacune interrogée par `#check` avec sa signature réelle, et sondée par `#print axioms` sur les théorèmes clés : uniquement les trois axiomes standards de Lean (`propext`, `Classical.choice`, `Quot.sound`), zéro `sorry`.\n", + "Le compagnon a visité **les déclarations des modules porteurs du converse** — `NormTails` (l'ancien point noir), `Converse` et `Bridge` — chacune interrogée par `#check` avec sa signature réelle, et sondée par `#print axioms` sur les théorèmes clés : uniquement les trois axiomes standards de Lean (`propext`, `Classical.choice`, `Quot.sound`), aucun `sorry`.\n", "\n", "Deux lectures à retenir :\n", "\n", @@ -2884,8 +2884,8 @@ "Les bornes théoriques y sont comparées aux fréquences empiriques — un bon\n", "test de cohérence entre théorie et simulation.\n", "\n", - "**Coût global du notebook** : ~10 secondes (lecture du lakefile + 20+\n", - "`#check` + 3 `#print axioms` + 4 `#eval Float`)." + "**Coût global du notebook** : ~10 secondes (lecture du lakefile +\n", + "`#check` + `#print axioms` + `#eval Float`)." ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb index 86ebb04807..dfb96fa239 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb @@ -437,7 +437,7 @@ "source": [ "## 3. La formalisation en Lean 4 - lectures des sources\n", "\n", - "Le theoreme de `Descent.lean` est **verifie** dans le lake (le README de `mimo_lean` l'annonce a 0 `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 verifie la proprete axiomatique des 5 theoremes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." + "Le theoreme de `Descent.lean` est **verifie** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 verifie la proprete axiomatique des theoremes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." ] }, { @@ -1470,7 +1470,7 @@ "\n", "L'instrumentation canonique pour compter les `sorry` reels d'un lake Lean est `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`). **JAMAIS `grep -c sorry`** : il compte la prose, pas le code (incidents fondateurs sur 21 lakes : 484 naifs pour 21 reels, dont 9 lakes a 0 reel).\n", "\n", - "Executer l'instrument sur le lake `mimo_lean` et verifier qu'il rapporte un compte compatible avec le verdict << 0 sorry formel >> du README du lake.\n", + "Executer l'instrument sur le lake `mimo_lean` et verifier qu'il rapporte un compte compatible avec le verdict de proprete du README du lake.\n", "\n", "**Indice 1 (commande)** : `subprocess.run([sys.executable, \"scripts/lean/count_code_sorry.py\", \"--json\"], cwd=ROOT_DIR, capture_output=True, text=True, timeout=30)`.\n", "\n", @@ -1519,7 +1519,7 @@ "\n", "1. **Patron transversal** (section 1, codes 1.1) - le teoreme **borne par le cout initial** le nombre de flips admissibles sous stricte decroissance. Trois substrats (recherche de temoin, revision argumentative, persona) illustrent ce patron sur des structures distinctes, et la grille valide empiriquement la conjonction `hstrict + hbarrier -> cible ET n_flips < M_N`.\n", "2. **Dissociation par echec d'hypothese** (section 2, code 2.1) - quand `hstrict` ou `hbarrier` **tombent**, le teoreme ne s'applique plus. Trois variantes demonstrent les symptomes (boucle, stagnation, divergence) et documentent la **dissociation** entre la garantie structurelle et l'atteinte par hasard.\n", - "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des 5 theoremes phares imprimees verbatim, verification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", + "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des theoremes phares imprimees verbatim, verification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", "4. **Pont cross-domain** (section 4) - le patron `ressource_initiale -> plafond_de_pas -> atteinte_ou_blocage` se retrouve au-dela du contexte MIMO : SMT/proveur Lean (cloture de goals), recherche de temoin, revision argumentative, persona. C'est cette **transversalite** qui fait la valeur pedagogique du teoreme : ce n'est pas un resultat d'algorithme specifique, c'est un patron structurel de garantie de terminaison sous decroissance stricte, et `Descent.lean` est sa formalisation canonique." ] }, diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb index 16a8e28088..05482f427b 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb @@ -104,8 +104,8 @@ "| « M₂₃ est un groupe de Galois sur ℚ » | **Xiaoyu Huang, Blake Jackson, Kyu-Hwan Lee, Bjorn Poonen, Rachel Pries, Shaowu Zhang** | Préprint arXiv:2608.08538, soumis le **9 août 2026** | Préprint arXiv (citation académique) |\n", "| Polynôme f₁ et script de vérification Magma | Les six auteurs du préprint | Dépôt [`shaowuz/m23isgalois`](https://github.com/shaowuz/m23isgalois), fichier `polynomial_f1.gp` | Code compagnon du préprint |\n", "\n", - "**Politique d'axiomes du dépôt amont** (mesurée à l'import, cf section 3) : `0 sorry`, `0 native_decide`,\n", - "`0 axiom` déclarés — la preuve repose uniquement sur les axiomes standard de Mathlib\n", + "**Politique d'axiomes du dépôt amont** (mesurée à l'import, cf section 3) : aucun `sorry`, aucun `native_decide`,\n", + "aucun `axiom` déclaré — la preuve repose uniquement sur les axiomes standard de Mathlib\n", "(`propext`, `Classical.choice`, `Quot.sound`). L'en-tête amont mentionne une assistance\n", "« Claude Code (Fable 5, 1M context) » dans le développement — conservée telle quelle." ] @@ -193,9 +193,9 @@ "### Interprétation\n", "\n", "Le lake `galois_lean` (toolchain v4.33.0, Mathlib épinglé) porte la preuve amont **vendored** :\n", - "le fichier `M23Lean4Web.lean` (~8 100 lignes) contient toute la couche M₂₂ dont dépend M₂₃,\n", + "le fichier `M23Lean4Web.lean` contient toute la couche M₂₂ dont dépend M₂₃,\n", "la construction de M₂₃ comme sous-groupe de Perm(23), sa cardinalité et sa simplicité.\n", - "Le compteur **0 sorry / 0 native_decide** confirme la politique d'axiomes annoncée : aucune\n", + "Le compteur d'import confirme la politique d'axiomes annoncée : aucune\n", "preuve trouée, aucune décision déléguée au noyau natif sans preuve." ] }, @@ -552,7 +552,7 @@ "4. **Spécialisation** (irréductibilité de Hilbert) : de ℚ(t) vers le ℚ du polynôme f₁.\n", "\n", "Le dépôt porte déjà le socle géométrique de cette chaîne dans\n", - "[`grothendieck_lean`](grothendieck_lean/README.md) (34 modules, 0 sorry) : sites, faisceaux,\n", + "[`grothendieck_lean`](grothendieck_lean/README.md) : sites, faisceaux,\n", "cohomologie — mais **pas** le π₁ étale ni l'existence de Riemann. La phrase qui doit rester\n", "noir sur blanc : **« M₂₃ est un groupe de Galois sur ℚ » n'est PAS formalisé dans ce dépôt** —\n", "il est prouvé dans le préprint, et vérifié computationnellement ci-dessous au niveau du\n", @@ -1548,7 +1548,7 @@ "\n", "La signature de `lowerRamificationGroup_antitone` imprimée par Lean dit l'essentiel : `Antitone (lowerRamificationGroup R G)` — **plus on monte dans la tour, plus le groupe rétrécit**. Et `lowerRamificationGroup_zero_eq_inertia` ancre le pied de la tour : le niveau 0 EST l'inertie, la ramification inférieure est son raffinement quantitatif. Enfin `iInf_lowerRamificationGroup_eq_bot` ferme la tour : un automorphisme invisible à **tous** les niveaux est l'identité — la filtration sépare les points de `G`.\n", "\n", - "Là encore, les `#print axioms` ne listent que la liste blanche standard. Ces 21 déclarations étaient le « trou » de visibilité du lake `galois_lean` au scanner de l'EPIC #11703 : elles sont désormais exécutées, auditées, et reliées à la complétion adique qui les motive — la théorie locale de Serre, lisible depuis le companion du problème inverse de Galois." + "Là encore, les `#print axioms` ne listent que la liste blanche standard. Ces déclarations étaient le « trou » de visibilité du lake `galois_lean` au scanner de l'EPIC #11703 : elles sont désormais exécutées, auditées, et reliées à la complétion adique qui les motive — la théorie locale de Serre, lisible depuis le companion du problème inverse de Galois." ] }, { @@ -1572,7 +1572,7 @@ "| **Énoncé 1** | M₂₃ simple, d'ordre 10 200 960 | Théorèmes Lean exécutés (`card_M23`, `simple_M23`), `#print axioms` = liste blanche standard | **PROUVÉ** (mécaniquement) |\n", "| **Énoncé 2** | M₂₃ groupe de Galois sur ℚ | Préprint cité + f₁ vérifié computationnellement (degré, irréductibilité, séparabilité, Frobenius) | **CITÉ** (non formalisé ; identification 23T5 = Magma, non reproduite) |\n", "| **Pont** | Le design de Witt S(4,7,23) | 253 heptades extraites, propriété S(4,7,23) échantillonnée, `PreservesHeptads` = définition formelle de M₂₃ | **Vérifié des deux côtés** |\n", - "| **Annexes A-B** | Complétion adique (`AdicCompletionLocalRing`, 27 déclarations) + tour de ramification inférieure (`LowerRamificationGroup`, 21) | 48 `#check` + 6 `#print axioms` exécutés par Lean (axiomes = liste blanche), troncatures 2-adiques rejouées en Python | **EXÉCUTÉ** (mécaniquement) |\n", + "| **Annexes A-B** | Complétion adique (`AdicCompletionLocalRing`) + tour de ramification inférieure (`LowerRamificationGroup`) | `#check` + `#print axioms` exécutés par Lean (axiomes = liste blanche), troncatures 2-adiques rejouées en Python | **EXÉCUTÉ** (mécaniquement) |\n", "\n", "Le problème inverse de Galois sporadique est refermé au sens mathématique (préprint du\n", "9 août 2026) — mais sa formalisation complète (existence de Riemann, descente, spécialisation\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23b-Lean-ERC20-Native-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23b-Lean-ERC20-Native-Companion.ipynb index e73ce089dd..5c3c6dfc60 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23b-Lean-ERC20-Native-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23b-Lean-ERC20-Native-Companion.ipynb @@ -22,7 +22,7 @@ "\n", "Le kernel `lean4-wsl` lance le REPL Lean **directement avec le `LEAN_PATH` du lake** : les modules compilés (`ERC20.State`, `ERC20.Ops`, `ERC20.Invariant`) sont résolus depuis `.lake/build/lib`. Convention du kernel (cf. Lean-21b) : les `import` se font **seuls, en tête de la première cellule code** — le REPL les traite comme l'en-tête d'un fichier source, ce qui charge réellement les oleans (le chargement de la fermeture Mathlib complète prend de l'ordre de la minute).\n", "\n", - "On importe les trois modules du lake plutôt que la racine `ERC20` : le `lakefile.lean` ne liste que `.submodules ERC20` et `ERC20_en` dans ses globs — le module racine français n'est pas un target de build (asymétrie signalée, les trois sous-modules couvrent les 17 déclarations)." + "On importe les modules du lake plutôt que la racine `ERC20` : le `lakefile.lean` ne liste que `.submodules ERC20` et `ERC20_en` dans ses globs — le module racine français n'est pas un target de build (asymétrie signalée, les sous-modules couvrent les déclarations)." ], "id": "d0b5feb6" }, @@ -596,9 +596,9 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "## 4. Le module `ERC20.Invariant` — la préservation prouvée (11 déclarations)\n", + "## 4. Le module `ERC20.Invariant` — la préservation prouvée\n", "\n", - "On `#check` les onze déclarations du module, en commençant par les deux `inductive` (`Op`, `Reachable`) : un extracteur à la main qui n'attrape que `theorem|lemma|def|abbrev` en compte 15 sur 17 — le piège mesuré sur le compagnon Python. Ici c'est le kernel qui résout les noms : la couverture ne peut pas mentir." + "On `#check` les déclarations du module, en commençant par les `inductive` (`Op`, `Reachable`) : un extracteur à la main qui n'attrape que `theorem|lemma|def|abbrev` en sous-compte — le piège mesuré sur le compagnon Python. Ici c'est le kernel qui résout les noms : la couverture ne peut pas mentir." ], "id": "d4d12562" }, @@ -1150,7 +1150,7 @@ "| L'invariant | traces jouets en Python | `example ... := by decide` **sous Lean** |\n", "| La trace | simulation Python | `Op`/`Reachable`/théorème **type-checkés** |\n", "\n", - "Les 17 déclarations du lake (3 `State`, 3 `Ops`, 11 `Invariant`, 0 racine) sont couvertes : chaque nom cité ci-dessus a été résolu par le kernel dans les cellules code 4–18. Les deux compagnons coexistent — la préférence de forme est « idéalement on veut les deux » (#11703) : le Python pour l'arc pédagogique et le Monte-Carlo, le natif pour la garantie du compilateur." + "Les déclarations du lake sont couvertes : chaque nom cité ci-dessus a été résolu par le kernel dans les cellules code 4–18. Les deux compagnons coexistent — la préférence de forme est « idéalement on veut les deux » (#11703) : le Python pour l'arc pédagogique et le Monte-Carlo, le natif pour la garantie du compilateur." ], "id": "732fac46" },