From 258f5b60d9bc42be033c969f799b2f70eb8a0670 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Thu, 8 Oct 2026 07:18:02 +0200 Subject: [PATCH] Fix(#18053): tranche Lean -- DANGLING_INTRO Lean-01-Setup cell[3] + INTERP_BEFORE_CODE Lean-7b-Examples cell[21] MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lean-01-Setup cell[3] : la phrase finale promettait le code « suivant » mais cell[4] est la table des plateformes (markdown) ; reformulee pour nommer la position reelle du bloc de diagnostic (cell[5]). Lean-7b-Examples cell[21] : « Interpretation de la solution » decrivait correction_loop_solution, definie nulle part avant elle (grep dossier Lean : 0 definition) -- l'Exercice 2 qui la vise est 11 cellules plus bas. Titre et chapeau reformules : presentation prospective de l'architecture attendue, plus lecture d'une sortie inexistante. Markdown-only : cellules code byte-identiques (8+11), ids preserves, pas de re-execution due (C.3). scan_cell_ordering : 2 findings MED elimines ; residuel LOW SECTION_GAP 7.7 hors scope (numerotation, pas ordre code/interp). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb | 2 +- .../SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb index 69ffc21705..851fd88dd1 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-01-Setup-Lean-Python.ipynb @@ -171,7 +171,7 @@ "| **lean4_jupyter** | Kernel Jupyter pour Lean | Oui |\n", "| **Kernel enregistre** | Lean dans Jupyter | Oui |\n", "\n", - "Executez la cellule suivante pour diagnostiquer votre environnement :" + "Le bloc de code « Diagnostic complet de l'environnement Lean 4 », apres la table des plateformes supportees, execute ce diagnostic." ] }, { diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb index cd1b0cd8c3..1f2447c987 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb @@ -1258,11 +1258,11 @@ "tags": [] }, "source": [ - "### Interprétation de la solution\n", + "### Architecture de la boucle de correction\n", "\n", - "**Fonction `correction_loop_solution`:**\n", + "**Fonction `correction_loop_solution`** (la cible de l'Exercice 2, en fin de carnet) :\n", "\n", - "Cette fonction implémente un prompt de correction itératif en 4 parties:\n", + "Elle construit un prompt de correction itératif en 4 parties :\n", "\n", "1. **Contexte de l'échec** - Indique que la preuve a échoué\n", "2. **Théorème cible** - Rappelle l'objectif à atteindre\n",