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 434d478f37..f77d7c0af8 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 @@ -32,7 +32,7 @@ "\n", "### Une seule source de verite : `Life.lean`\n", "\n", - "Le coeur de Life — la règle B3/S23, les patterns, leurs invariants — est défini **une seule fois**, formellement, dans les modules Lean `conway_lean/Conway/Life*.lean`. Les simulations Python `numpy`/`matplotlib` de ce notebook ne sont **pas** une seconde définition concurrente : ce sont des **illustrations** qui donnent l'intuition visuelle (animations, grilles, contours). Quand on veut une **certitude** (et non une intuition), on interroge directement le `.lean` : la section 9.7 lance `#eval` sur les predicats Lean réels, et la section 10 lance `lake build`. Règle de lecture : **le notebook illustre, `Life.lean` prouvé.**\n", + "Le coeur de Life — la règle B3/S23, les patterns, leurs invariants — est défini **une seule fois**, formellement, dans les modules Lean `conway_lean/Conway/Life*.lean`. Les simulations Python `numpy`/`matplotlib` de ce notebook ne sont **pas** une seconde définition concurrente : ce sont des **illustrations** qui donnent l'intuition visuelle (animations, grilles, contours). Quand on veut une **certitude** (et non une intuition), on interroge directement le `.lean` : la section 9.7 lance `#eval` sur les predicats Lean réels, et la section 10 lance `lake build`. Règle de lecture : **le notebook illustre, `Life.lean` prouve.**\n", "\n", "### Plan\n", "\n", @@ -370,7 +370,7 @@ "source": [ "### Interpretation : le blinker comme oscillateur période 2\n", "\n", - "Le **blinker** est le plus petit oscillateur non-trivial de Life : 3 cellules alignees. Toutes les 2 generations, il oscille entre orientation horizontale et verticale. La vérification `g2 == g0` ci-dessus est une **illustration numérique** sur grille bornee : elle *montre* la periodicite sur un cas concret, elle ne la *prouvé* pas (une seule grille, finie).\n", + "Le **blinker** est le plus petit oscillateur non-trivial de Life : 3 cellules alignees. Toutes les 2 generations, il oscille entre orientation horizontale et verticale. La vérification `g2 == g0` ci-dessus est une **illustration numérique** sur grille bornee : elle *montre* la periodicite sur un cas concret, elle ne la *prouve* pas (une seule grille, finie).\n", "\n", "$$\\text{step}^2(\\text{blinker}) = \\text{blinker} \\quad \\text{(propriété illustree ici, prouvée en Lean)}$$\n", "\n", @@ -380,7 +380,7 @@ "theorem blinker_period_two : isOscillator blinker_h 2 = true := by native_decide\n", "```\n", "\n", - "Le predicat `isOscillator g n := evolve n g == g` retourne un `Bool` sur le type `List (Int x Int)` ; `native_decide` le compile en code natif et tranche `true` en un éclair (cf section 9 pour le choix `List` plutot que `Finset`). **Le notebook illustre ; `Life.lean` prouvé.**" + "Le predicat `isOscillator g n := evolve n g == g` retourne un `Bool` sur le type `List (Int x Int)` ; `native_decide` le compile en code natif et tranche `true` en un éclair (cf section 9 pour le choix `List` plutot que `Finset`). **Le notebook illustre ; `Life.lean` prouve.**" ] }, { @@ -773,7 +773,7 @@ " expand (hashlife_step mc) = step^[2^n] (center_region (expand mc))\n", "```\n", "\n", - "Cette preuve est l'invariant central de l'Epic : tout le reste (Gemini, OTCA, Beluchenko CPU digital) en derive par `native_decide` sur des temoins concrets. La preuve elle-même se fait par induction sur le niveau $n$ + analyse de cas du step central 4x4 (décide pour $n = 2$, induction pour $n + 1$)." + "Cette preuve est l'invariant central de l'Epic : tout le reste (Gemini, OTCA, Beluchenko CPU digital) en derive par `native_decide` sur des temoins concrets. La preuve elle-même se fait par induction sur le niveau $n$ + analyse de cas du step central 4x4 (decide pour $n = 2$, induction pour $n + 1$)." ] }, { @@ -1075,10 +1075,10 @@ "\n", "- **Paul Rendell, avril 2000** : la première machine de Turing explicite construite dans Life - le witness telechargeable ci-dessous.\n", "- **Nicolay Beluchenko / Andy Stearns, 2016** : un **CPU digital** programmable construit a partir d'OTCA metapixels, executant un cycle en 1 048 576 generations. Ce CPU est le temoin `cpu_witness` declare dans `Conway.Life.Pillars.lean` (Phase 8 cible).\n", - "- **Nicholas Carlini, 2020** : un CPU 8 bits complet (ROM, RAM, ALU, registres, horloge), de l'ordre de $10^6$ cellules - indépendant du CPU de Beluchenko/Stearns. Trop massif pour être rendu ou décide ici, c'est le sommet de la discipline.\n", + "- **Nicholas Carlini, 2020** : un CPU 8 bits complet (ROM, RAM, ALU, registres, horloge), de l'ordre de $10^6$ cellules - indépendant du CPU de Beluchenko/Stearns. Trop massif pour être rendu ou decide ici, c'est le sommet de la discipline.\n", "- **Adam P. Goucher, additionneur Spartan** : environ 5 000 cellules, cible pragmatique pour la preuve Lean.\n", "\n", - "Le deuxieme prodige, c'est le **calcul** proprement dit. Des 1970, Conway conjecturait que Life était Turing-complète ; Paul Rendell l'a prouvé *par construction* en 2000 en batissant une vraie machine de Turing - ruban, tete de lecture, table de transitions - entierement en cellules B3/S23. Vingt ans plus tard, Carlini est alle au bout de l'idee avec un microprocesseur 8 bits fonctionnel.\n", + "Le deuxieme prodige, c'est le **calcul** proprement dit. Des 1970, Conway conjecturait que Life était Turing-complète ; Paul Rendell l'a prouve *par construction* en 2000 en batissant une vraie machine de Turing - ruban, tete de lecture, table de transitions - entierement en cellules B3/S23. Vingt ans plus tard, Carlini est alle au bout de l'idee avec un microprocesseur 8 bits fonctionnel.\n", "\n", "| Caractéristique | Machine de Turing (Rendell) | CPU digital (Beluchenko/Stearns) |\n", "|-----------------|------------------------------|----------------------------------|\n", @@ -1088,7 +1088,7 @@ "| Niveau quadtree (estimé) | ~10 | ~12 |\n", "| Ce qu'il démontre | Turing-completude constructive | CPU programmable dans Life |\n", "\n", - "Pour la preuve formelle, on ne vise pas le CPU complet (le binaire `native_decide` n'y tiendrait pas) : on commence par l'**additionneur Spartan** de Goucher, assez petit pour être décide, et on remonte si la machine suit.\n", + "Pour la preuve formelle, on ne vise pas le CPU complet (le binaire `native_decide` n'y tiendrait pas) : on commence par l'**additionneur Spartan** de Goucher, assez petit pour être decide, et on remonte si la machine suit.\n", "\n", "**Théorème cible Lean** (additionneur, Phase 8) :\n", "```lean\n", @@ -1289,7 +1289,7 @@ "| II | Turing / calculateurs (2000-2020) | calcul universel | Life calcule n'importe quoi |\n", "| III | Gemini (Wade, 2010) | self-replication | Life se recopie elle-même |\n", "\n", - "La beaute de l'histoire tient a leur **emboitement**, et l'ordre est une montee en puissance. L'Acte I prouvé que Life peut faire tourner Life. L'Acte II prouvé 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", + "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 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", @@ -1299,12 +1299,12 @@ "\n", "| Nom prospectif (section 6) | Nom réel dans `Pillars.lean` | Statut |\n", "|----------------------------|------------------------------|--------|\n", - "| `otca_self_emulates` | `otca_metapixel_witness` | prouvé (vide) - Phase 7 réel |\n", - "| `spartan_adder_correct` | `cpu_witness` (Beluchenko/Stearns) | prouvé (vide) - Phase 8 réel |\n", - "| `gemini_replicates` | `gemini_witness` | prouvé (vide) - Phase 6 réel |\n", - "| — | `unitcell_witness` (Beluchenko 2011) | prouvé (vide) - Phase 8 réel |\n", + "| `otca_self_emulates` | `otca_metapixel_witness` | prouve (vide) - Phase 7 réel |\n", + "| `spartan_adder_correct` | `cpu_witness` (Beluchenko/Stearns) | prouve (vide) - Phase 8 réel |\n", + "| `gemini_replicates` | `gemini_witness` | prouve (vide) - Phase 6 réel |\n", + "| — | `unitcell_witness` (Beluchenko 2011) | prouve (vide) - Phase 8 réel |\n", "\n", - "> **Statut compile = prouvé contre grilles vides.** Les temoins compilent **sans `sorry`** : `otcaInitial` / `otcaTarget` etc. sont des grilles vides (`([] : Grid)`), donc `evolveHashlifeFastMemo N [] = []` est prouvé trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. La **preuve réelle** - 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 prouvé trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. La **preuve réelle** - 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 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 complète.\n", "\n", @@ -1486,7 +1486,7 @@ "source": [ "### Interpretation : le scaffold Lean des piliers (sans sorry)\n", "\n", - "Le fichier `Pillars.lean` encode les temoins communautaires comme des **théorèmes prouves** (sans sorry). L'import `Conway.Life.RLE` est actif, et un **temoin prouvé non trivial** (`pulsar_period3`) démontre 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 **théorèmes prouves** (sans sorry). L'import `Conway.Life.RLE` est actif, et un **temoin prouve non trivial** (`pulsar_period3`) démontre que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur un vrai pattern.\n", "\n", "Structure de chaque temoin :\n", "\n", @@ -1497,7 +1497,7 @@ "\n", "theorem otca_metapixel_witness :\n", " evolveHashlifeFastMemo otcaGens otcaInitial = otcaTarget :=\n", - " evolveHashlifeFastMemo_empty otcaGens -- prouvé : evolveHashlifeFastMemo N [] = []\n", + " evolveHashlifeFastMemo_empty otcaGens -- prouve : evolveHashlifeFastMemo N [] = []\n", "```\n", "\n", "Les `Initial` et `Target` sont des grilles vides (`[]`) : comme `otcaInitial = otcaTarget = []`, le théorème se reduit a `evolveHashlifeFastMemo N [] = []`, resolu par le lemme `evolveHashlifeFastMemo_empty`. **Aucun `sorry`, aucun axiome admis** - le module compile sans sorry. Les RLE réels (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 réelle.\n", @@ -1513,7 +1513,7 @@ "\n", "> **Statut compile vs statut mathematique.** Les théorèmes sont *syntaxiquement prouves* (sans sorry, pas d'axiome) parce qu'ils portent sur des grilles vides. La **preuve substantielle** - le pattern RLE réel 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 réel ».\n", "\n", - "#### Le temoin prouvé non trivial : `pulsar_period3`\n", + "#### Le temoin prouve non trivial : `pulsar_period3`\n", "\n", "Le pipeline est déjà valide sur un pattern réel de taille moderee :\n", "\n", @@ -1523,7 +1523,7 @@ " native_decide\n", "```\n", "\n", - "Ce théorème utilise `RLE.pulsar_parsed` (48 cellules réelles) et prouvé la periodicite du pulsar par `native_decide`. Contrairement aux 4 piliers (grilles vides), `pulsar_period3` porte sur un **vrai pattern** : il constitue la **preuve de concept** que le pipeline RLE -> Grid -> evolveHashlifeFast fonctionne de bout en bout sur données réelles.\n", + "Ce théorème utilise `RLE.pulsar_parsed` (48 cellules réelles) et prouve la periodicite du pulsar par `native_decide`. Contrairement aux 4 piliers (grilles vides), `pulsar_period3` porte sur un **vrai pattern** : il constitue la **preuve de concept** que le pipeline RLE -> Grid -> evolveHashlifeFast fonctionne de bout en bout sur données réelles.\n", "\n", "#### Roadmap : des preuves triviales aux preuves réelles\n", "\n", @@ -1534,7 +1534,7 @@ "| 3 | `HashlifeCorrectness.lean` | Théorème central P4 (`hashlifeResultAux_correct`) | P4 Prouvé ; P5 (`hashlife_correct`) reste en sorry |\n", "| 4 | Chaque temoin | `by native_decide` sur le pattern réel | En attente des étapes 1-3 |\n", "\n", - "Le chemin vers les preuves réelles est donc : **HashlifeMemo operationnel -> chargement RLE -> native_decide -> temoin prouvé sur pattern réel**. Le temoin pulsar confirme que l'infrastructure RLE -> Grid est prete ; il reste a rendre la memoization tractable pour les patterns geants.\n" + "Le chemin vers les preuves réelles est donc : **HashlifeMemo operationnel -> chargement RLE -> native_decide -> temoin prouve sur pattern réel**. Le temoin pulsar confirme que l'infrastructure RLE -> Grid est prete ; il reste a rendre la memoization tractable pour les patterns geants.\n" ] }, { @@ -2011,7 +2011,7 @@ "\n", "> **`#eval` interprete vs `native_decide`.** Le `#eval` ci-dessus exerce l'**interprete** Lean : il convient aux predicats peu profonds (quelques generations). Le pentadecathlon, lui, demande 15 generations : son `#eval` interprete serait lent, alors que le théorème `pentadecathlon_period_15 : isOscillator pentadecathlon 15 = true := by native_decide` (section 10) **compile** la decision en code natif — c'est tout l'intérêt de `native_decide`. On laisse donc ce cas a la preuve compilee de la section 10.\n", "\n", - "Contrairement aux vérifications numpy (qui *illustrent* sur une grille bornee), ces `#eval` exercent le code formellement vérifié : si l'un retournait `false`, le théorème correspondant serait faux. C'est la différence entre « le notebook montre » et « Life.lean prouvé »." + "Contrairement aux vérifications numpy (qui *illustrent* sur une grille bornee), ces `#eval` exercent le code formellement vérifié : si l'un retournait `false`, le théorème correspondant serait faux. C'est la différence entre « le notebook montre » et « Life.lean prouve »." ] }, { @@ -2218,17 +2218,17 @@ "tags": [] }, "source": [ - "### 9.8 Le parseur RLE *prouvé* : `#eval parseRLE` (source de verite vs re-implémentation Python)\n", + "### 9.8 Le parseur RLE *prouve* : `#eval parseRLE` (source de verite vs re-implémentation Python)\n", "\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 prouvé** : `Conway.Life.RLE.parseRLE : String -> Except String Grid` (fichier `conway_lean/Conway/Life/RLE.lean`, **sans `sorry`**). Mieux : le module accompagne le parseur de **théorèmes 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 **théorèmes de correction** fermes par `native_decide` :\n", "\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 prouvé**, pas une coincidence observee a l'oeil.\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", - "La cellule ci-dessous interroge directement cette source de verite : on `#eval` le vrai `parseRLE` sur les chaînes RLE des patterns (glider, LWSS, pulsar, canon de Gosper) et on retrouve les comptes de cellules attendus (5, 9, 48, 36) ainsi que l'égalité round-trip. C'est la différence entre « le notebook parse en Python pour dessiner » et « Lean parse et *prouvé* que le parse est correct »." + "La cellule ci-dessous interroge directement cette source de verite : on `#eval` le vrai `parseRLE` sur les chaînes RLE des patterns (glider, LWSS, pulsar, canon de Gosper) et on retrouve les comptes de cellules attendus (5, 9, 48, 36) ainsi que l'égalité round-trip. C'est la différence entre « le notebook parse en Python pour dessiner » et « Lean parse et *prouve* que le parse est correct »." ] }, { @@ -2745,8 +2745,8 @@ "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`. Théorème bridge `hashlifeResultMemo_correct` **prouvé** (extraction d'un lemme auxiliaire valide `cacheOK_empty`, sans sorry).\n", - "3. **`evolveHashlifeFastMemo`** : entrée top-level pour le chemin rapide memoise. Théorème `evolveHashlifeFastMemo_eq_evolveHashlifeFast` **prouvé** (même mécanisme, sans sorry).\n", + "2. **`hashlifeResultMemo : MacroCell -> StateM MemoCache MacroCell`** : version memoisee de `hashlifeResultAux`. Théorème bridge `hashlifeResultMemo_correct` **prouve** (extraction d'un lemme auxiliaire valide `cacheOK_empty`, sans sorry).\n", + "3. **`evolveHashlifeFastMemo`** : entrée top-level pour le chemin rapide memoise. Théorème `evolveHashlifeFastMemo_eq_evolveHashlifeFast` **prouve** (même mécanisme, sans sorry).\n", "4. **Des théorèmes-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", @@ -2755,7 +2755,7 @@ "\n", " Chaque preuve est *trivialement vraie* (grilles vides : `evolveHashlifeFastMemo N [] = []`). La preuve **réelle** - pattern RLE charge, `by native_decide` - est l'objectif des Phases 6-8 une fois la memoization operationnelle.\n", "\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 réel reste a faire. A contraster avec `pulsar_period3` (section 9.8), seul temoin prouvé 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 réel 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** : 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",