From 7e6a6e6f3955dbca563fa872bee1fdd68daa6fb7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 14 Oct 2026 07:35:29 +0200 Subject: [PATCH] fix(prose,#5081): README SymbolicAI -- clause Serre100 au futur alors que #17789 est merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lean-37-Capstone-Serre100 livre depuis le 25/09 (#17789) : la phrase d'annonce « la presentera et y renverra » devient le present accompli, avec lien direct vers le carnet. La clause « modele pour Conway et Grothendieck » reste vraie (aucun de ces capstones livre). Co-Authored-By: Claude Sonnet 5.5 --- MyIA.AI.Notebooks/SymbolicAI/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/README.md b/MyIA.AI.Notebooks/SymbolicAI/README.md index 2cca36d4bb..ea18180a91 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/README.md @@ -150,7 +150,7 @@ Chaque série se présente en trois temps : ce qu'elle apprend, son **parcours l - **Parcours léger** — 1 à 6, les fondations : installation, types dépendants, propositions et preuves (Curry-Howard), quantificateurs, mode tactique, Mathlib4. Puis 7 à 10, la preuve à l'ère des LLMs : intégration LLM, preuve agentique, orchestration multi-agents, LeanDojo. - **Chapitres thématiques** — à partir de 11, chaque numéro ouvre un chapitre qui suppose les fondations et se choisit selon son intérêt : réseaux de neurones vérifiés (11), théorème de sensibilité de Huang (12), contextualité de Kochen-Specker (13), hommages à Grothendieck (15) et à Conway (16), théorie des nœuds (17), puis les digestions de résultats récents (Sendov, *Analysis I* de Tao, PFR, détection MIMO, problème inverse de Galois pour M₂₃…). - **Pour approfondir** — les lettres sont surtout des **compagnons** : un compagnon Lean natif (`-Native`, kernel Lean) qui prouve ce que le notebook principal raconte, ou un compagnon Python qui l'illustre. Les preuves vivent dans des **lakes** (`sensitivity_lean`, `conway_lean`, `knot_lean`, `grothendieck_lean`, `galois_lean`…). -- **Sous-série** — [Serre100](Lean/Serre100/README.md) a sa propre numérotation et son lake `serre100_lean`. Un notebook d'escalier dans le parcours principal la présentera et y renverra (#17789). Ce modèle doit ensuite servir aux familles de chapitres les plus denses, comme Conway et Grothendieck. +- **Sous-série** — [Serre100](Lean/Serre100/README.md) a sa propre numérotation et son lake `serre100_lean`. Le notebook d'escalier du parcours principal la présente et y renvoie ([Lean-37-Capstone-Serre100](Lean/Lean-37-Capstone-Serre100.ipynb), #17789). Ce modèle doit ensuite servir aux familles de chapitres les plus denses, comme Conway et Grothendieck. - [README de la série Lean](Lean/README.md) ### SMT / Z3 — décider sous contraintes