Skip to content

fix(search,#13841): minimal rename Lean-18 -> Search-03e + README attribution fix #14250

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jsboige merged 1 commit into from
Sep 2, 2026
Merged

fix(search,#13841): minimal rename Lean-18 -> Search-03e + README attribution fix #14250

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 2 additions & 4 deletions MyIA.AI.Notebooks/Search/Applications/Hybrid/App-22-AlgorithmSelection-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -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": {
Expand Down
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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*
Expand Down
34 changes: 17 additions & 17 deletions ...ons/Lean-18-Search-AStar-Optimality.ipynb → ...dations/Search-03e-AStar-Optimality.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand All @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
},
{
Expand Down Expand Up @@ -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"
]
}
],
Expand Down Expand Up @@ -1619,13 +1619,13 @@
"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"
}
},
"nbformat": 4,
"nbformat_minor": 5
}
}
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Search/index.qmd
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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/`.
Expand Down
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Sendov-Complex-Analysis.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -1220,4 +1220,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-MIMO-Detection-Flips.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)."
]
}
Expand All @@ -1908,4 +1908,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-24-ERC20-Invariant-Companion.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)`."
]
}
],
Expand Down
Loading
Loading