diff --git a/MyIA.AI.Notebooks/Search/Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb b/MyIA.AI.Notebooks/Search/Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb index 0e5af55946..37a7eec0d0 100644 --- a/MyIA.AI.Notebooks/Search/Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb +++ b/MyIA.AI.Notebooks/Search/Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb @@ -1366,13 +1366,12 @@ "|---|---|---|---|\n", "| **Performance empirique** | Quel solveur réussit, à quel coût observé ? | [Sudoku-18](../../../Sudoku/Sudoku-18-Comparison-Python.ipynb), [Sudoku-18b](../../../Sudoku/Sudoku-18b-Statistical-Comparison-Python.ipynb) | Comparaison et incertitude sur un protocole ; aucune preuve universelle. |\n", "| **Correction / invariants** | Une étape de propagation conserve-t-elle les solutions ? | [Sudoku-19-Lean-Propagation](../../../Sudoku/Sudoku-19-Lean-Propagation.ipynb) | Formalise des invariants de propagation ; **ne vérifie pas** les implémentations de Théodore. |\n", - "| **Optimalité conditionnelle** | Sous quelles hypothèses une stratégie est-elle optimale ? | [Lean-18-Search-AStar-Optimality](../../Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb) | Prouve une optimalité sous hypothèses (heuristique admissible, modèle formel) ; ne transforme pas un chrono en théorème. |\n", + "| **Optimalité conditionnelle** | Sous quelles hypothèses une stratégie est-elle optimale ? | [Search-03e-AStar-Optimality](../../Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Prouve une optimalité sous hypothèses (heuristique admissible, modèle formel) ; ne transforme pas un chrono en théorème. |\n", "| **Valeur d'un jeu adverse** | Comment relier valeur minimax et stratégie ? | [GameTheory-05b-Lean-Minimax](../../../GameTheory/GameTheory-05b-Lean-Minimax.ipynb) | Donne les fondations formelles de minimax ; ne certifie ni le moteur Puissance 4 ni ses performances. |\n", "| **Décision** | Comment arbitrer entre attributs et coût d'information ? | [DecInfer-02-Lean-ExpectedUtility](../../../Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb), [DecInfer-06](../../../Probas/DecisionTheory/DecInfer/DecInfer-06-Value-Information.ipynb) | Formalise le langage du choix ; les poids et distributions restent à justifier empiriquement. |\n", "\n", "Cette séparation évite deux confusions symétriques : **un solveur rapide n'est pas, pour cette raison, prouvé correct** ; **un algorithme prouvé correct ou optimal sous hypothèses n'est pas, pour cette raison, le plus rapide ici**. Le prolongement naturel serait un pipeline où une preuve borne l'espace des candidats admissibles, puis où la sélection empirique arbitre entre les candidats certifiés.\n" ] - }, { "cell_type": "markdown", @@ -1542,9 +1541,8 @@ "- **Terrains applicatifs** :\n", " - [App-20-SudokuBenchmark-Python](../CSP/App-20-SudokuBenchmark-Python.ipynb), [App-14b-ConnectFour](../Search/App-14b-ConnectFour.ipynb), [App-14-ConnectFour-Adversarial](../Search/App-14-ConnectFour-Adversarial.ipynb), [App-7-Wordle](../CSP/App-7-Wordle.ipynb).\n", "- **Ponts formels, sans certification du code étudiant** :\n", - " - [Sudoku-19-Lean-Propagation](../../../Sudoku/Sudoku-19-Lean-Propagation.ipynb), [Lean-18-Search-AStar-Optimality](../../Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb), [GameTheory-05b-Lean-Minimax](../../../GameTheory/GameTheory-05b-Lean-Minimax.ipynb), [DecInfer-02-Lean-ExpectedUtility](../../../Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb).\n" + " - [Sudoku-19-Lean-Propagation](../../../Sudoku/Sudoku-19-Lean-Propagation.ipynb), [Search-03e-AStar-Optimality](../../Part1-Foundations/Search-03e-AStar-Optimality.ipynb), [GameTheory-05b-Lean-Minimax](../../../GameTheory/GameTheory-05b-Lean-Minimax.ipynb), [DecInfer-02-Lean-ExpectedUtility](../../../Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb).\n" ] - } ], "metadata": { diff --git a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md index 43ebd43615..a78c8a65a1 100644 --- a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md +++ b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md @@ -17,9 +17,9 @@ hors `_en` ; bascule #11688 — historiquement `standalone-tactic` ; les mention | `discrepancy_lean` | v4.32.1 | 0 | 8 | 0² | PEDA/REF | #12823 | | **Total** | — | **0** | **13** | **1** | — | — | -¹ Notebook câblé : **Lean-18-Search-AStar-Optimality.ipynb** +¹ Notebook câblé : **Search-03e-AStar-Optimality.ipynb** (`Search/Part1-Foundations/`, descente tranche 1 #13662 depuis -`SymbolicAI/Lean/`). Companion conceptuel = la série **Search** (CSP/Foundations, +`SymbolicAI/Lean/`, rename par #13841). Companion conceptuel = la série **Search** (CSP/Foundations, A* vs BFS sur terrain pondéré — convention sibling-lake). Répond aussi au prong-B de l'Epic [#3801](https://github.com/jsboige/CoursIA/issues/3801) : démontrer le moteur A* sur un problème non-trivial (heuristique discriminante), pas un graphe à coût uniforme où A* diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb similarity index 95% rename from MyIA.AI.Notebooks/Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb rename to MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb index b30a553037..adb42c0694 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb @@ -14,7 +14,7 @@ "tags": [] }, "source": [ - "# Lean-18 : A* et l'optimalité sous heuristique admissible — visite formelle de `search_lean`\n", + "# Search-03e : A* et l'optimalité sous heuristique admissible — visite formelle de `search_lean`\n", "\n", "**Navigation** : [<< Lean-17b Knots Invariants](../../SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb) | [Index](README.md)\n", "\n", @@ -31,7 +31,7 @@ "\n", "***\n", "\n", - "**Le pont** : Lean-18 ↔ Lean-6 (Mathlib / `NNReal`, `List`, `linarith`) ↔ Lean-12b (cérémonie `#check` / `#print axioms`, c.8256) ↔ Search-3-Informed (A* heuristique en Python, vue empirique). Lean-18 est la version *formelle* de Search-3 : on calcule les chemins en Python sur des cas concrets, on prouve l'optimalité en Lean.\n" + "**Le pont** : Search-03e ↔ Lean-6 (Mathlib / `NNReal`, `List`, `linarith`) ↔ Lean-12b (cérémonie `#check` / `#print axioms`, c.8256) ↔ Search-3-Informed (A* heuristique en Python, vue empirique). Search-03e est la version *formelle* de Search-3 : on calcule les chemins en Python sur des cas concrets, on prouve l'optimalité en Lean.\n" ] }, { @@ -73,7 +73,7 @@ "\n", "***\n", "\n", - "**Le pont** : A* unifie BFS / UCS / Dijkstra / A* dans un cadre unique. Lean-12b (Sensitivity) unifie aussi 4 techniques distinctes en un seul cadre. Lean-18 reprend la structure 4-modules (vocabulaire / lemme / théorème / portée) de Lean-12b mais pour l'algorithmique plutôt que l'algèbre linéaire. Search-3-Informed est la sister empirique.\n" + "**Le pont** : A* unifie BFS / UCS / Dijkstra / A* dans un cadre unique. Lean-12b (Sensitivity) unifie aussi 4 techniques distinctes en un seul cadre. Search-03e reprend la structure 4-modules (vocabulaire / lemme / théorème / portée) de Lean-12b mais pour l'algorithmique plutôt que l'algèbre linéaire. Search-3-Informed est la sister empirique.\n" ] }, { @@ -400,7 +400,7 @@ "\n", "***\n", "\n", - "**Le pont** : `NNReal` est utilisé dans Lean-6 (Mathlib / `Data.NNReal`) pour toute mesure d'une grandeur physique (durée, coût, probabilité). Lean-18 l'instancie pour les poids d'arêtes. Search-3-Informed et App-2-GraphColoringemploient `Real` ou `Int` en Python — Lean-18 est plus rigoureux sur la non-négativité.\n" + "**Le pont** : `NNReal` est utilisé dans Lean-6 (Mathlib / `Data.NNReal`) pour toute mesure d'une grandeur physique (durée, coût, probabilité). Search-03e l'instancie pour les poids d'arêtes. Search-3-Informed et App-2-GraphColoringemploient `Real` ou `Int` en Python — Search-03e est plus rigoureux sur la non-négativité.\n" ] }, { @@ -523,7 +523,7 @@ "\n", "***\n", "\n", - "**Le pont** : `pathCost` est `Finset.sum` en Lean-6 (Mathlib / BigOperators), et `PathFrom` est `List.Chain` en Lean-6 (Mathlib / Data.List.Chain). Lean-18 les spécialise pour les graphes pondérés. Search-3-Informed calcule `pathCost` explicitement en Python sur des cas concrets.\n" + "**Le pont** : `pathCost` est `Finset.sum` en Lean-6 (Mathlib / BigOperators), et `PathFrom` est `List.Chain` en Lean-6 (Mathlib / Data.List.Chain). Search-03e les spécialise pour les graphes pondérés. Search-3-Informed calcule `pathCost` explicitement en Python sur des cas concrets.\n" ] }, { @@ -559,7 +559,7 @@ "\n", "***\n", "\n", - "**Le pont** : l'admissibilité est `∀ n, h n ≤ hStar n` en Lean-6 (Mathlib, un simple `∀`). La consistance est `∀ n m, h n ≤ edge n m + h m` (idem). Lean-18 ne réinvente rien — il **instancie** les concepts de Lean-6 dans le cadre des graphes pondérés. Search-3-Informed vérifie empiriquement l'admissibilité sur des exemples concrets.\n" + "**Le pont** : l'admissibilité est `∀ n, h n ≤ hStar n` en Lean-6 (Mathlib, un simple `∀`). La consistance est `∀ n m, h n ≤ edge n m + h m` (idem). Search-03e ne réinvente rien — il **instancie** les concepts de Lean-6 dans le cadre des graphes pondérés. Search-3-Informed vérifie empiriquement l'admissibilité sur des exemples concrets.\n" ] }, { @@ -707,7 +707,7 @@ "\n", "***\n", "\n", - "**Le pont** : `zero_admissible` est l'archétype du lemme trivial mais pédagogiquement crucial. Lean-6 (Mathlib) regorge de tels lemmes (`add_zero`, `mul_one`, etc.) qui ancrent les structures algébriques. Lean-18 ancre la théorie A* dans un lemme analogue. Search-3-Informed illustre les trois heuristiques (`h ≡ 0`, euclidienne, Manhattan) en Python.\n" + "**Le pont** : `zero_admissible` est l'archétype du lemme trivial mais pédagogiquement crucial. Lean-6 (Mathlib) regorge de tels lemmes (`add_zero`, `mul_one`, etc.) qui ancrent les structures algébriques. Search-03e ancre la théorie A* dans un lemme analogue. Search-3-Informed illustre les trois heuristiques (`h ≡ 0`, euclidienne, Manhattan) en Python.\n" ] }, { @@ -739,7 +739,7 @@ "\n", "***\n", "\n", - "**Le pont** : la structure induction sur les listes + lemme auxiliaire est la même qu'en Lean-6 / `Mathlib.Data.List`. Lean-12b utilise la même structure pour la sensibilité booléenne. Lean-18 l'instancie pour A*. Search-3-Informed illustre cette optimalité empiriquement sur des graphes concrets.\n" + "**Le pont** : la structure induction sur les listes + lemme auxiliaire est la même qu'en Lean-6 / `Mathlib.Data.List`. Lean-12b utilise la même structure pour la sensibilité booléenne. Search-03e l'instancie pour A*. Search-3-Informed illustre cette optimalité empiriquement sur des graphes concrets.\n" ] }, { @@ -905,7 +905,7 @@ "\n", "***\n", "\n", - "**Le pont** : l'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib`. Le lemme auxiliaire `suffix_pathFrom` est un `List.drop` + induction. Lean-18 ne réinvente rien — il utilise les primitives de Lean-6 sur le type `PathFrom`. Lean-12b (Sensitivity) utilise exactement la même structure pour ses preuves spectrales.\n" + "**Le pont** : l'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib`. Le lemme auxiliaire `suffix_pathFrom` est un `List.drop` + induction. Search-03e ne réinvente rien — il utilise les primitives de Lean-6 sur le type `PathFrom`. Lean-12b (Sensitivity) utilise exactement la même structure pour ses preuves spectrales.\n" ] }, { @@ -943,7 +943,7 @@ "\n", "***\n", "\n", - "**Le pont** : la récurrence sur la queue est `List.recOn` (Lean-6 / Mathlib). La tactique `linarith` est Lean-6 / `Mathlib.Tactic.Linarith`. Lean-18 ne dépend que de Lean-6 pour ces preuves. Lean-12b (Sensitivity) utilise la même mécaniquepour les preuves spectrales (`f² = n Id` puis optimalité).\n" + "**Le pont** : la récurrence sur la queue est `List.recOn` (Lean-6 / Mathlib). La tactique `linarith` est Lean-6 / `Mathlib.Tactic.Linarith`. Search-03e ne dépend que de Lean-6 pour ces preuves. Lean-12b (Sensitivity) utilise la même mécaniquepour les preuves spectrales (`f² = n Id` puis optimalité).\n" ] }, { @@ -1148,7 +1148,7 @@ "\n", "***\n", "\n", - "**Le pont** : `linarith` est `Mathlib.Tactic.Linarith` en Lean-6. L'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib.Data.List`. Lean-18 est **structurellement** un Lean-6 (Mathlib) instance : il ne réinvente aucune tactique, il assemble les primitives existantes pour A*. Lean-12b fait pareil pour la sensibilité.\n" + "**Le pont** : `linarith` est `Mathlib.Tactic.Linarith` en Lean-6. L'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib.Data.List`. Search-03e est **structurellement** un Lean-6 (Mathlib) instance : il ne réinvente aucune tactique, il assemble les primitives existantes pour A*. Lean-12b fait pareil pour la sensibilité.\n" ] }, { @@ -1191,7 +1191,7 @@ "\n", "***\n", "\n", - "**Le pont** : Lean-18 et Lean-12b sont **structurellement jumeaux** : 4 modules, preuve par induction sur les listes, théorème final issu d'une accumulation locale → globale. C'est le **template** de la série Lean : un grand théorème décomposé en 4 modules factorisés pour réutilisation.\n" + "**Le pont** : Search-03e et Lean-12b sont **structurellement jumeaux** : 4 modules, preuve par induction sur les listes, théorème final issu d'une accumulation locale → globale. C'est le **template** de la série Lean : un grand théorème décomposé en 4 modules factorisés pour réutilisation.\n" ] }, { @@ -1222,7 +1222,7 @@ "\n", "***\n", "\n", - "**Le pont** : Search-3-Informed (Python, sister de Lean-18) illustre la même triade d'exercices (prédiction, reproduction, contre-exemple) sur le même sujet A*. Lean-18 est la **version formelle** de Search-3 : ce qu'on observe empiriquement en Python est **prouvé** en Lean dans ce notebook.\n" + "**Le pont** : Search-3-Informed (Python, sister de Search-03e) illustre la même triade d'exercices (prédiction, reproduction, contre-exemple) sur le même sujet A*. Search-03e est la **version formelle** de Search-3 : ce qu'on observe empiriquement en Python est **prouvé** en Lean dans ce notebook.\n" ] }, { @@ -1573,7 +1573,7 @@ "\n", "***\n", "\n", - "**Le pont** : Lean-18 ↔ Lean-12b (cérémonie commune) ↔ Lean-6 (Mathlib / primitives `List`, `NNReal`, `linarith`) ↔ Search-3-Informed (vue empirique Python du même sujet). Lean-18 ferme la boucle : on a maintenant la version *formelle* et la version *empirique* de l'optimalité A*, comparables et complémentaires. Lean-13 (Kochen-Specker) et Lean-14 (Finiteness) poursuivent la série Lean avec d'autres théorèmes.\n" + "**Le pont** : Search-03e ↔ Lean-12b (cérémonie commune) ↔ Lean-6 (Mathlib / primitives `List`, `NNReal`, `linarith`) ↔ Search-3-Informed (vue empirique Python du même sujet). Search-03e ferme la boucle : on a maintenant la version *formelle* et la version *empirique* de l'optimalité A*, comparables et complémentaires. Lean-13 (Kochen-Specker) et Lean-14 (Finiteness) poursuivent la série Lean avec d'autres théorèmes.\n" ] } ], @@ -1619,8 +1619,8 @@ "end_time": "2026-07-03T08:57:32.976590", "environment_variables": {}, "exception": null, - "input_path": "Lean-18-Search-AStar-Optimality.ipynb", - "output_path": "Lean-18-Search-AStar-Optimality.ipynb", + "input_path": "Search-03e-AStar-Optimality.ipynb", + "output_path": "Search-03e-AStar-Optimality.ipynb", "parameters": {}, "start_time": "2026-07-03T08:50:38.893396", "version": "2.6.0" @@ -1628,4 +1628,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/Search/index.qmd b/MyIA.AI.Notebooks/Search/index.qmd index 868fc9c9c6..b2335007ff 100644 --- a/MyIA.AI.Notebooks/Search/index.qmd +++ b/MyIA.AI.Notebooks/Search/index.qmd @@ -73,7 +73,7 @@ heuristique **admissible puis consistante** (0 sorry de production, prong-B Epic [#3801](https://github.com/jsboige/CoursIA/issues/3801) : terrain pondéré où l'heuristique discrimine, pas un cas dégénéré où A\* ≡ BFS). Le companion de la série Search est : -- [Lean-18-Search-AStar-Optimality](Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb) +- [Search-03e-AStar-Optimality](Part1-Foundations/Search-03e-AStar-Optimality.ipynb) — visite formelle Python de `search_lean`, descente tranche 1 [#13662](https://github.com/jsboige/CoursIA/issues/13662) depuis `SymbolicAI/Lean/`. diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb index 38cf4575e3..c2dfd1467c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb @@ -26,7 +26,7 @@ "\n", "| Notebook precedent | Notebook suivant |\n", "|---|---|\n", - "| [Lean-18 - Recherche A* Optimalite](../../Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb) | Lean-20 (a venir) |\n", + "| [Lean-18 - Recherche A* Optimalite](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Lean-20 (a venir) |\n", "\n", "***\n", "\n", @@ -1220,4 +1220,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb index f905b3465c..17d678d009 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb @@ -1882,7 +1882,7 @@ " Hanson-Wright, mesures gaussiennes -- dependance externe de la Phase 3b.\n", "- **Mathlib 4** : `MeasureTheory`, `ProbabilityTheory`, espaces de Hilbert.\n", "- Notebooks associes : [Lean-21 (PFR)](Lean-21-PFR-Entropy-Method.ipynb),\n", - " [Lean-18 (A*)](../../Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb),\n", + " [Lean-18 (A*)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb),\n", " [Lean-6 (Mathlib)](Lean-6-Mathlib-Essentials.ipynb)." ] } @@ -1908,4 +1908,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-ERC20-Invariant-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-ERC20-Invariant-Companion.ipynb index 8608d39a94..8b6a4b1e18 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-ERC20-Invariant-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-ERC20-Invariant-Companion.ipynb @@ -1379,7 +1379,7 @@ "- **Lake `erc20_lean`** (`MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/`) — la version Lean 4 + Mathlib : `ERC20/State.lean` (modèle), `ERC20/Ops.lean` (transitions), `ERC20/Invariant.lean` (préservation).\n", "- **EPIC #4980** — convention i18n Lean (aggrégateur bilingue inline FR-EN dans `ERC20.lean`, sibling pair dans `ERC20_en.lean`).\n", "- **Rule C.6** (mandat user 2026-08-19) — préférence pour un compagnon kernel `lean4-wsl` à côté du notebook Python ; le pattern actuel (subprocess `lake env lean`) reste mergeable, le kernel Lean natif est une suite à explorer.\n", - "- Notebooks associés : `[Lean-23 (Galois)](Lean-23-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-22 (MIMO)](Lean-22-MIMO-Detection-Flips.ipynb)`, `[Lean-21 (PFR)](Lean-21-PFR-Entropy-Method.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[Lean-18 (A*)](../../Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb)`." + "- Notebooks associés : `[Lean-23 (Galois)](Lean-23-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-22 (MIMO)](Lean-22-MIMO-Detection-Flips.ipynb)`, `[Lean-21 (PFR)](Lean-21-PFR-Entropy-Method.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[Lean-18 (A*)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`." ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index da9290429a..84f72c5a41 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -132,7 +132,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | # | Notebook | Contenu | Durée | |---|----------|---------|-------| -| 18 | [Lean-18-Search-AStar-Optimality](../../Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb) | Optimalité de A* sous heuristique admissible : graphe pondéré ℝ≥0 et coût additif `pathCost`, prédicats `Admissible`/`Consistent`, théorème phare `admissible_implies_optimal` (borne en f), téléscopage `consistent_implies_path_bound` + monotonie de f - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 35 min | +| 18 | [Search-03e-AStar-Optimality](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Optimalité de A* sous heuristique admissible : graphe pondéré ℝ≥0 et coût additif `pathCost`, prédicats `Admissible`/`Consistent`, théorème phare `admissible_implies_optimal` (borne en f), téléscopage `consistent_implies_path_bound` + monotonie de f - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 35 min | ### Partie 7 : Digestions de résultats profonds et companions (Sendov, Tao, PFR, MIMO, Galois, ERC-20, calibration, décision, Hopf S⁶) @@ -415,7 +415,7 @@ Lean/ ├── Lean-17-Knots-a-Conway-and-Proofs.ipynb # Python kernel - Conway, les nœuds et la preuve de Piccirillo (noeud de Conway) ├── Lean-17b-Knots-Invariants-Companion.ipynb # Python kernel - invariants de nœuds (PD-codes, Reidemeister, Fox tricolorability), compagnon knot_lean ├── Lean-17c-Knots-Companion-Formel.ipynb # Python kernel - companion formel knot_lean (modules non cités par 17b, murs R2/R3, miroir i18n) -├── Lean-18-Search-AStar-Optimality.ipynb # Python kernel - optimalité de A* sous heuristique admissible (companion search_lean, 0 sorry) +├── Search-03e-AStar-Optimality.ipynb # Python kernel - optimalité de A* sous heuristique admissible (companion search_lean, 0 sorry) ├── Lean-19-Sendov-Complex-Analysis.ipynb # Python kernel - conjecture de Sendov (preuve Mazur 2026, digestion et formalisation Tao) ├── Lean-20-Analysis-I-Tao-Workflow.ipynb # Python kernel - le lac Analysis I de Tao (architecture, 5 lemmes emblématiques) ├── Lean-21-PFR-Entropy-Method.ipynb # Python kernel - conjecture PFR (méthode entropique, #check réels du lac compilé) diff --git a/MyIA.AI.Notebooks/SymbolicAI/README.md b/MyIA.AI.Notebooks/SymbolicAI/README.md index e4211508be..6d69719e59 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/README.md @@ -228,7 +228,7 @@ Série de **33 notebooks** sur **Lean 4**, proof assistant basé sur la théorie | 16e | [Lean-16e-Conway-FRACTRAN-Lean-Native](Lean/Lean-16e-Conway-FRACTRAN-Lean-Native.ipynb) | Lean 4 / WSL | Port natif Lean de FRACTRAN : encodage fractions, machine à fractions, premiers programmes | 3 | | 17 | [Lean-17-Knots-a-Conway-and-Proofs](Lean/Lean-17-Knots-a-Conway-and-Proofs.ipynb) | Python WSL | Noeuds de Conway : introduction, énoncés, premier port formel adossé à `conway_knots_lean/` | 3 | | 17b | [Lean-17b-Knots-Invariants-Companion](Lean/Lean-17b-Knots-Invariants-Companion.ipynb) | Python WSL | Companion natif : invariants de noeuds, snippets WSL, sources `conway_knots_lean/` | 3 | -| 18 | [Lean-18-Search-AStar-Optimality](../Search/Part1-Foundations/Lean-18-Search-AStar-Optimality.ipynb) | Lean 4 / WSL | Preuve d'optimalité A* dans le lake `planners_lean` : consistance, admissibilité, branchement | 3 | +| 18 | [Search-03e-AStar-Optimality](../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Python 3 | Optimalité de A* sous heuristique admissible/consistante : graphe pondéré ℝ≥0, `pathCost` additif, prédicats `Admissible`/`Consistent`, théorèmes phares `admissible_implies_optimal` + `consistent_implies_path_bound` - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 3 | | **Théorèmes phares 2026** | | | | | | 19 | [Lean-19-Sendov-Complex-Analysis](Lean/Lean-19-Sendov-Complex-Analysis.ipynb) | Python WSL | Conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques, contexte de la preuve | 4 | | 20 | [Lean-20-Analysis-I-Tao-Workflow](Lean/Lean-20-Analysis-I-Tao-Workflow.ipynb) | Python WSL | Manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 4 | diff --git a/docs/curriculum/_inventory.md b/docs/curriculum/_inventory.md index c9ac7e3a7d..d4c5929560 100644 --- a/docs/curriculum/_inventory.md +++ b/docs/curriculum/_inventory.md @@ -38,7 +38,7 @@ | 4 | `MyIA.AI.Notebooks/Probas/README.md` L74-119 | Apprenant inférence probabiliste multi-stack (Infer.NET + PyMC) | Phase 1-3 (~17h) + 4 alternatifs | Phases narratives + « Parcours alternatifs » (data scientist, théorie décision, comparatif, rapide) | **RELOCATE** — couple racine + DecisionTheory/Causal-Bridges pour le pilote symbolique causal | | 5 | `MyIA.AI.Notebooks/Probas/PyMC/README.md` L197-221 | Data scientist Python ~10h | 4 parcours distincts | 4 « Quel parcours choisir » à structure parfaite (data scientist / décision / comparatif / rapide) | **RELOCATE** — modèle compact, à reprendre dans `docs/curriculum/aima-walk.md` comme annexe probabiliste | | 6 | `MyIA.AI.Notebooks/Probas/DecisionTheory/README.md` L36 | Apprenant théorie de la décision (fondations → pont causal) | Non chiffré | Phases narratives | **INTEGRATE** — récits dans parcours symbolique (causal bridges) | -| 7 | `MyIA.AI.Notebooks/SymbolicAI/Lean/README.md` (sub) | Lean 4 multi-domain (knots, mimo, conway, social_choice, asymmetric_info) | Variable selon lake | Structure + lacs nommés | **INTEGRATE** — référencé par `aima-walk.md` pour les compagnons formels (cf `Lean-18-Search-AStar-Optimality` cf #13685) | +| 7 | `MyIA.AI.Notebooks/SymbolicAI/Lean/README.md` (sub) | Lean 4 multi-domain (knots, mimo, conway, social_choice, asymmetric_info) | Variable selon lake | Structure + lacs nommés | **INTEGRATE** — référencé par `aima-walk.md` pour les compagnons formels (cf `Search-03e-AStar-Optimality` cf #13685 + #13841 rename) | | 8 | `MyIA.AI.Notebooks/SymbolicAI/Lean/social_choice_lean/LEAN_PREREQUISITES.md` L7-119 | Débutant Lean / Mathlib / reproduction | 3 parcours numérotés (Débutant / Intermédiaire / Avancé) | « Parcours N » structuré (3 niveaux nommés) | **RELOCATE** — modèle le plus progressif du dépôt, à utiliser pour le pilote symbolique | | 9 | `MyIA.AI.Notebooks/SymbolicAI/README.md` L61-83 | Apprenant IA symbolique général | Pont LLM ~4h + Apprentissage symbolique ~9h30 | « Parcours alternatifs » cross-série | **INTEGRATE** — narratif connecteur entre Tweety / Lean / Planners / SmartContracts | | 10 | `MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md` L74-110 | Apprenant logique argumentative | Variable (cf alternatifs) | « Parcours alternatifs » | **INTEGRATE** — premier pas du pilote symbolique | diff --git a/docs/notebook-metadata/production-scope.md b/docs/notebook-metadata/production-scope.md index cd8d89c2f1..3b56c10482 100644 --- a/docs/notebook-metadata/production-scope.md +++ b/docs/notebook-metadata/production-scope.md @@ -293,7 +293,7 @@ l'Epic) ; un dossier de revue est alors préparé (T2).* - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-15-Grothendieck-Tribute.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17-Knots-a-Conway-and-Proofs.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17b-Knots-Invariants-Companion.ipynb` -- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Search-AStar-Optimality.ipynb` +- [ ] `MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Analysis-I-Tao-Workflow.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-PFR-Entropy-Method.ipynb`