jsboige · jsboige · May 30, 2026 · May 30, 2026
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-1-Setup.ipynb
@@ -29,8 +29,15 @@
     "5. **Lean-5-Tactics** - Construction de preuves par tactiques\n",
     "6. **Lean-6-Mathlib-Essentials** - Bibliotheque mathematique Mathlib4\n",
     "7. **Lean-7-LLM-Integration** - Integration avec les LLMs\n",
+    "7b. **Lean-7b-Examples** - Exemples grandeur nature (AlphaProof, LeanDojo)\n",
     "8. **Lean-8-Agentic-Proving** - Agents autonomes pour preuves\n",
-    "9. **Lean-9-LeanDojo** - LeanDojo pour ML/LLM theorem proving\n",
+    "9. **Lean-9-SK-Multi-Agents** - Semantic Kernel multi-agents\n",
+    "10. **Lean-10-LeanDojo** - LeanDojo pour ML/LLM theorem proving\n",
+    "11. **Lean-11-TorchLean** - PyTorch + Lean (reasoning vs learning)\n",
+    "12. **Lean-12-Sensitivity-Theorem** - Theoreme de sensibilite\n",
+    "13. **Lean-13-Grothendieck-Tribute** - Hommage a Alexandre Grothendieck\n",
+    "14. **Lean-14-Conway-Tribute** - Hommage a John Conway (Game of Life)\n",
+    "15. **Lean-15-Kochen-Specker** - Theoreme de Kochen-Specker\n",
     "\n",
     "**Public vise:** Etudiants, chercheurs interesses par la verification formelle et les assistants de preuves.\n",
     "\n",
@@ -1787,4 +1794,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 4
-}
+}
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-14-Conway-Tribute.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-14-Conway-Tribute.ipynb
@@ -13,7 +13,7 @@
     },
     "tags": []
    },
-   "source": "# Lean-14 : Hommage a John Conway — Game of Life as Computation\n\n**Navigation** : [<< Lean-12 Sensitivity](Lean-12-Sensitivity-Theorem.ipynb) | [Lean-13 Grothendieck >>](Lean-13-Grothendieck-Tribute.ipynb) | [Lean-15 Kochen-Specker >>](Lean-15-Kochen-Specker.ipynb) | [Index](README.md)\n\n**Kernel** : Python 3 (illustrations + verifications combinatoires) + Lean 4 (via WSL pour section 11)\n\n---\n\n## Introduction\n\nJohn Horton Conway (1937 - 2020) est sans doute le mathematicien qui aura le plus brouille la frontiere entre les jeux et les structures profondes des mathematiques. Cambridge puis Princeton, il a invente le **Game of Life** en 1970 avec un groupe d'etudiants autour de lui : Michael Guy, Richard Guy, et plusieurs joueurs d'Othello. Sa mort en avril 2020, foudroyee par la COVID, a fait basculer la communaute combinatoire en deuil et accelere les hommages formels.\n\nL'Epic #1151 a ouvert 5 noix moins celebres de Conway en Lean 4 : l'algorithme du Doomsday, la suite Look-and-Say, le langage FRACTRAN, les positions de Nim, le probleme de l'ange. Mais **l'oeuvre la plus iconique de Conway manquait au catalogue** : le Game of Life lui-meme.\n\nCe notebook couvre les phases initiales de l'Epic #1647 (\"Hommage Conway : Life-as-Computation\"). Il pose les fondations Lean du Game of Life dans `conway_lean/Conway/Life.lean`, et trace la feuille de route vers les piliers communautaires : Gemini (Wade 2010), OTCA Metapixel (Due 2006), 8-bit computer (Carlini 2020).\n\n### Plan\n\n1. Tour des 5 noix Phase 1 (Doomsday, FRACTRAN, Look-and-Say, Nim, Ange) - `#check` Lean\n2. La regle Game of Life B3/S23 - definition Python + simulation\n3. Visualisation : still-lifes, oscillateurs, vaisseaux (blinker, glider, etc.)\n4. Spartan logic, gating sur cells stationnaires, flux de gliders\n5. Intuition hashlife : macrocells, canonicalisation, complexite logarithmique\n6. Les 3 piliers communautaires (Gemini, OTCA, Carlini CPU)\n7. Turing-completude : Conway 1982, Rendell 2000, Springer 2016\n8. Demo : blinker (periode 2) et glider (periode 4) en Python animes\n9. Le port Lean : `Life.lean`, definitions et premiers theoremes\n10. Verification : `lake build Conway.Life` + grep sorry\n11. Pont vers les phases ulterieures de l'Epic\n\n### Prerequis\n\n- Notions de cellules d'automates cellulaires (utile mais pas indispensable)\n- Notebooks Lean-1 a Lean-7 pour les aspects formels (recommande)\n- Lean-12 pour le pattern Lake build + WSL\n\n### Duree estimee : 60 minutes"
+   "source": "# Lean-14 : Hommage a John Conway — Game of Life as Computation\n\n**Navigation** : [<< Lean-13 Grothendieck](Lean-13-Grothendieck-Tribute.ipynb) | [Index](README.md) | [Lean-15 Kochen-Specker >>](Lean-15-Kochen-Specker.ipynb)\n\n**Kernel** : Python 3 (illustrations + verifications combinatoires) + Lean 4 (via WSL pour section 11)\n\n---\n\n## Introduction\n\nJohn Horton Conway (1937 - 2020) est sans doute le mathematicien qui aura le plus brouille la frontiere entre les jeux et les structures profondes des mathematiques. Cambridge puis Princeton, il a invente le **Game of Life** en 1970 avec un groupe d'etudiants autour de lui : Michael Guy, Richard Guy, et plusieurs joueurs d'Othello. Sa mort en avril 2020, foudroyee par la COVID, a fait basculer la communaute combinatoire en deuil et accelere les hommages formels.\n\nL'Epic #1151 a ouvert 5 noix moins celebres de Conway en Lean 4 : l'algorithme du Doomsday, la suite Look-and-Say, le langage FRACTRAN, les positions de Nim, le probleme de l'ange. Mais **l'oeuvre la plus iconique de Conway manquait au catalogue** : le Game of Life lui-meme.\n\nCe notebook couvre les phases initiales de l'Epic #1647 (\"Hommage Conway : Life-as-Computation\"). Il pose les fondations Lean du Game of Life dans `conway_lean/Conway/Life.lean`, et trace la feuille de route vers les piliers communautaires : Gemini (Wade 2010), OTCA Metapixel (Due 2006), 8-bit computer (Carlini 2020).\n\n### Plan\n\n1. Tour des 5 noix Phase 1 (Doomsday, FRACTRAN, Look-and-Say, Nim, Ange) - `#check` Lean\n2. La regle Game of Life B3/S23 - definition Python + simulation\n3. Visualisation : still-lifes, oscillateurs, vaisseaux (blinker, glider, etc.)\n4. Spartan logic, gating sur cells stationnaires, flux de gliders\n5. Intuition hashlife : macrocells, canonicalisation, complexite logarithmique\n6. Les 3 piliers communautaires (Gemini, OTCA, Carlini CPU)\n7. Turing-completude : Conway 1982, Rendell 2000, Springer 2016\n8. Demo : blinker (periode 2) et glider (periode 4) en Python animes\n9. Le port Lean : `Life.lean`, definitions et premiers theoremes\n10. Verification : `lake build Conway.Life` + grep sorry\n11. Pont vers les phases ulterieures de l'Epic\n\n### Prerequis\n\n- Notions de cellules d'automates cellulaires (utile mais pas indispensable)\n- Notebooks Lean-1 a Lean-7 pour les aspects formels (recommande)\n- Lean-12 pour le pattern Lake build + WSL\n\n### Duree estimee : 60 minutes"
   },
   {
    "cell_type": "markdown",

diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Kochen-Specker.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Kochen-Specker.ipynb
@@ -13,7 +13,7 @@
     },
     "tags": []
    },
-   "source": "# Lean-15 : Le Theoreme de Kochen-Specker (Cabello 18 vecteurs)\n\n**Navigation** : [<< Lean-12 Sensitivity](Lean-12-Sensitivity-Theorem.ipynb) | [Lean-13 Grothendieck](Lean-13-Grothendieck-Tribute.ipynb) | [Lean-14 Conway](Lean-14-Conway-Tribute.ipynb) | [Index](README.md)\n\n**Kernel** : Python 3 (illustrations + verifications combinatoires) + Lean 4 (WSL) pour la section 6\n\n---\n\n## Introduction\n\nEn 1967, Simon Kochen et Ernst Specker publient un theoreme qui exclut une large classe d'interpretations de la mecanique quantique : les **theories a variables cachees non-contextuelles**. La preuve originale utilise **117 vecteurs** de R^3. Plusieurs raffinements suivent (33 vecteurs par Peres 1991, 20 par Kernaghan 1994) jusqu'a la preuve la plus compacte connue avec **18 vecteurs de R^4** par Cabello, Estebaranz et Garcia-Alcaine en 1996. C'est cette derniere qui sert de noyau combinatoire au theoreme de libre arbitre de Conway-Kochen (2006).\n\nCe notebook est le **Pilier 1** de l'Epic #1651 (Theoreme de Libre Arbitre Conway-Kochen). Il presente :\n1. La question : peut-on attribuer une valeur 0/1 aux observables quantiques de maniere non-contextuelle ?\n2. La structure : 18 vecteurs de R^4 en 9 bases orthogonales, chacun appartenant a exactement 2 bases\n3. L'argument de parite : 9 (impair) vs 2k (pair) -- contradiction\n4. Verification computationnelle : aucune coloration valide n'existe sur 2^18 essais\n5. Le port Lean 4 (Pilier 1 du theoreme de libre arbitre)\n6. Verification `lake build` du scaffold\n7. Pont avec le theoreme de libre arbitre de Conway-Kochen (Piliers 2-3)\n\n### Prerequis\n- Notions d'algebre lineaire (R^4, bases orthogonales, produit scalaire)\n- Notebooks Lean-1 a Lean-7 pour les aspects formels (recommande)\n- Lean-12 pour le pattern Lake build + WSL\n\n### Duree estimee : 75 minutes"
+   "source": "# Lean-15 : Le Theoreme de Kochen-Specker (Cabello 18 vecteurs)\n\n**Navigation** : [<< Lean-14 Conway Tribute](Lean-14-Conway-Tribute.ipynb) | [Index](README.md)\n\n**Kernel** : Python 3 (illustrations + verifications combinatoires) + Lean 4 (WSL) pour la section 6\n\n---\n\n## Introduction\n\nEn 1967, Simon Kochen et Ernst Specker publient un theoreme qui exclut une large classe d'interpretations de la mecanique quantique : les **theories a variables cachees non-contextuelles**. La preuve originale utilise **117 vecteurs** de R^3. Plusieurs raffinements suivent (33 vecteurs par Peres 1991, 20 par Kernaghan 1994) jusqu'a la preuve la plus compacte connue avec **18 vecteurs de R^4** par Cabello, Estebaranz et Garcia-Alcaine en 1996. C'est cette derniere qui sert de noyau combinatoire au theoreme de libre arbitre de Conway-Kochen (2006).\n\nCe notebook est le **Pilier 1** de l'Epic #1651 (Theoreme de Libre Arbitre Conway-Kochen). Il presente :\n1. La question : peut-on attribuer une valeur 0/1 aux observables quantiques de maniere non-contextuelle ?\n2. La structure : 18 vecteurs de R^4 en 9 bases orthogonales, chacun appartenant a exactement 2 bases\n3. L'argument de parite : 9 (impair) vs 2k (pair) -- contradiction\n4. Verification computationnelle : aucune coloration valide n'existe sur 2^18 essais\n5. Le port Lean 4 (Pilier 1 du theoreme de libre arbitre)\n6. Verification `lake build` du scaffold\n7. Pont avec le theoreme de libre arbitre de Conway-Kochen (Piliers 2-3)\n\n### Prerequis\n- Notions d'algebre lineaire (R^4, bases orthogonales, produit scalaire)\n- Notebooks Lean-1 a Lean-7 pour les aspects formels (recommande)\n- Lean-12 pour le pattern Lake build + WSL\n\n### Duree estimee : 75 minutes"
   },
   {
    "cell_type": "markdown",

diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb
@@ -3633,6 +3633,15 @@
    "metadata": {},
    "execution_count": 17,
    "outputs": []
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "---\n",
+    "\n",
+    "**Navigation** : [← Lean-6-Mathlib-Essentials](Lean-6-Mathlib-Essentials.ipynb) | [Index](Lean-1-Setup.ipynb) | [Lean-8-Agentic-Proving →](Lean-8-Agentic-Proving.ipynb)\n"
+   ]
   }
  ],
  "metadata": {

diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md
@@ -2,12 +2,12 @@
 
 <!-- CATALOG-STATUS
 series: SymbolicAI-Lean
-pedagogical_count: 16
-breakdown: Fondations=5, Etat-de-l-art=6, Applications=3, Kochen-Specker=1, Tribute=1
-maturity: PRODUCTION=6, BETA=10
+pedagogical_count: 17
+breakdown: Fondations=5, Etat-de-l-art=6, Applications=3, Kochen-Specker=1, Tribute=2
+maturity: PRODUCTION=6, BETA=11
 -->
 
-Cette serie de **16 notebooks** introduit **Lean 4**, un assistant de preuves et langage de programmation fonctionnel base sur la theorie des types dependants, avec un focus sur les techniques modernes d'utilisation de LLMs pour l'assistance aux preuves, la verification formelle de reseaux de neurones, le port de theoremes phares (theoreme de Kochen-Specker, 18 vecteurs Cabello), et des hommages aux mathematiciens (Grothendieck, langage grothendieckien dans Mathlib 4).
+Cette serie de **17 notebooks** introduit **Lean 4**, un assistant de preuves et langage de programmation fonctionnel base sur la theorie des types dependants, avec un focus sur les techniques modernes d'utilisation de LLMs pour l'assistance aux preuves, la verification formelle de reseaux de neurones, le port de theoremes phares (theoreme de Kochen-Specker, 18 vecteurs Cabello), et des hommages aux mathematiciens (Grothendieck, langage grothendieckien dans Mathlib 4).
 
 ## Navigation
 
@@ -22,7 +22,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet
 | **Integration IA** | 1-7, 7b | ~5h | Ajoute LLMs, exemples et benchmarks |
 | **Complet** | 1-12 | ~11h | Toutes les fonctionnalites incluant LeanDojo et theoreme de sensibilite |
 | **Avec Pilier 1.B** | 1-12, 15 | ~12h | Inclut le port Kochen-Specker (Cabello 18-vecteurs) - contextuality quantique |
-| **Avec hommages** | 1-12, 13, 15 | ~12h45 | Ajoute Lean-13 (langage grothendieckien dans Mathlib 4) |
+| **Avec hommages** | 1-12, 13, 14, 15 | ~14h | Ajoute Lean-13 (Grothendieck) et Lean-14 (Conway, Game of Life) |
 
 ## Structure
 
@@ -61,8 +61,9 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet
 | # | Notebook | Contenu | Duree |
 |---|----------|---------|-------|
 | 13 | [Lean-13-Grothendieck-Tribute](Lean-13-Grothendieck-Tribute.ipynb) | Langage grothendieckien dans Mathlib 4 : categories/foncteurs, cribles et topologies de Grothendieck, faisceaux, schemas, site de Zariski, morphismes etales/lisses - Epic #1646 | 45 min |
+| 14 | [Lean-14-Conway-Tribute](Lean-14-Conway-Tribute.ipynb) | Hommage a John Conway : Game of Life as Computation, Doomsday, FRACTRAN, Look-and-Say, Nim, Angel - Epic #1647 | 60 min |
 
-**Duree totale** : ~12h45
+**Duree totale** : ~14h
 
 ## Acquis d'apprentissage
 
@@ -74,6 +75,7 @@ A l'issue de la serie, vous saurez :
 - **Tracer et explorer** une base de preuves a grande echelle : LeanDojo (parsing AST, theorem extraction, interaction Dojo), reseaux de neurones verifies via IBP/CROWN (TorchLean). Notebooks 10-11.
 - **Porter** un theoreme de recherche en Lean 4 : theoreme de sensibilite (Huang 2019, hypercube et signing matrix), theoreme de Kochen-Specker (Cabello 18 vecteurs, argument de parite, contextuality quantique). Notebooks 12, 15.
 - **Lire le langage grothendieckien** dans Mathlib 4 : categories et foncteurs, cribles et topologies de Grothendieck, faisceaux, schemas et sites, morphismes etales/lisses — comme entree vers la geometrie algebrique formalisee. Notebook 13.
+- **Explorer les noix de Conway** en Lean 4 : Game of Life as Computation, Doomsday, FRACTRAN, Look-and-Say, Nim, Angel — port formel de resultats combinatoires iconiques. Notebook 14.
 
 Pour l'etat formel detaille des modules support (preuves resolues vs `sorry` residuels), voir [LEAN_INVENTORY.md](../../GameTheory/LEAN_INVENTORY.md) et le [README du projet conway_lean](conway_lean/README.md).
 
@@ -96,6 +98,7 @@ Pour l'etat formel detaille des modules support (preuves resolues vs `sorry` res
 | 11a | TorchLean Python | ~45 | 3 | Oui | **COMPLET** |
 | 12 | Sensitivity-Theorem | ~31 | 4 | Non | **NOUVEAU** |
 | 13 | Grothendieck-Tribute | ~23 | 0 | - | **NOUVEAU** (hommage) |
+| 14 | Conway-Tribute | ~26 | 0 | - | **NOUVEAU** (hommage) |
 | 15 | Kochen-Specker | ~25 | 1 | 0 | **NOUVEAU** |
 
 Tous les notebooks incluent :
@@ -265,8 +268,9 @@ Lean/
 ├── Lean-11-TorchLean.ipynb         # Lean4 kernel - NN verification
 ├── Lean-11-TorchLean-Python.ipynb  # Python kernel - Implementation algorithmes
 ├── Lean-13-Grothendieck-Tribute.ipynb # Python kernel - hommage Grothendieck (langage grothendieckien Mathlib)
-├── _run_lean_snippet.sh            # Helper WSL : run Lean snippet avec cache Mathlib
+├── Lean-14-Conway-Tribute.ipynb   # Python kernel - hommage Conway (Game of Life as Computation)
 ├── Lean-15-Kochen-Specker.ipynb    # Lean4 kernel - theoreme de Kochen-Specker (Pilier 1.B)
+├── _run_lean_snippet.sh            # Helper WSL : run Lean snippet avec cache Mathlib
 ├── lean_runner.py                  # Module Python multi-backend
 ├── README.md
 ├── .env.example