diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb index 1a15e51fec..f5077c5bea 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16a-Conway-Man-and-Work.ipynb @@ -600,13 +600,13 @@ "|-------|---------|---------|\n", "| Doomsday | `Conway/DoomsdayLemmas.lean` | 5 théorèmes (annees bissextiles, jour de la mort de Conway) |\n", "| Look-and-Say | `Conway/LookAndSayLemmas.lean` | 3 théorèmes (chiffres <-> entier, terme 4) |\n", - "| Nim / nim-sum | `Conway/Nim.lean` | defs + 4 théorèmes + `#eval` |\n", + "| Nim / nim-sum | `Conway/Nim.lean` | defs + 15 théorèmes + `#eval` |\n", "| Problème de l'Ange | `Conway/Angel.lean` | defs + 4 théorèmes (cardinal du moveset) + `#eval` |\n", "| Game of Life (Phase 1) | `Conway/Life.lean` | 7 micro-preuves (block, blinker, glider...) |\n", "| MathlibMap | `Conway/MathlibMap.lean` | 10 `#check` Conway-adjacents dans Mathlib |\n", "\n", "Le depot heberge aussi un **second projet Lake indépendant**, `conway_cgt_lean/`\n", - "(toolchain `v4.31.0-rc2`), qui importe [`vihdzp/combinatorial-games`](https://github.com/vihdzp/combinatorial-games)\n", + "(toolchain `v4.33.0-rc1`), qui importe [`vihdzp/combinatorial-games`](https://github.com/vihdzp/combinatorial-games)\n", "et presente les résultats centraux de Conway en théorie des jeux :\n", "\n", "| Thème | Fichier | Contenu |\n", @@ -906,7 +906,7 @@ "\n", "Le **nim-sum** (XOR des tas) est la cle de la théorie de Sprague-Grundy : une position de Nim est\n", "perdante pour le joueur au trait **si et seulement si** son nim-sum est nul. Le fichier contient\n", - "les définitions, 4 théorèmes, et des `#eval` executables." + "les définitions, 15 théorèmes, et des `#eval` executables." ] }, { @@ -1514,7 +1514,7 @@ "\n", "Suivant le **pattern Peters** (cf. `social_choice_lean_peters/`), nous importons ce depot comme\n", "dépendance Lake sans dupliquer son code, et nous presentons ses résultats cles via le module\n", - "`CGTTour.lean`. Ce second projet Lake (`conway_cgt_lean/`, toolchain `v4.31.0-rc2`) est\n", + "`CGTTour.lean`. Ce second projet Lake (`conway_cgt_lean/`, toolchain `v4.33.0-rc1`) est\n", "indépendant de `conway_lean/` (`v4.33.0`).\n", "\n", "**Résultats formalises (13 `#check`) :**\n", @@ -1705,6 +1705,7 @@ }, { "cell_type": "markdown", + "id": "be806737", "metadata": {}, "source": [ "### Statut du build CGTTour (mesuré 06/10)\n",