diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb
index fc1d24a74d..13f16414df 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-7-LLM-Integration.ipynb
@@ -1514,67 +1514,7 @@
     "tags": []
    },
    "source": [
-    "### 6.4 Explications : Prompt Engineering pour Lean\n",
-    "\n",
-    "Le prompting efficace pour Lean necessite precision et structure. Voici les patterns cles :\n",
-    "\n",
-    "#### 1. Prompt initial : Contexte riche\n",
-    "\n",
-    "Un bon prompt initial inclut :\n",
-    "- **Imports disponibles** : Mathlib, tactiques standard\n",
-    "- **Variables et types** : `(a b : Nat)`, `(x : Real)`, etc.\n",
-    "- **Hypotheses** : Lemmes et faits déjà etablis\n",
-    "- **Théorème cible** : Formulation exacte\n",
-    "\n",
-    "**Exemple** :\n",
-    "```\n",
-    "Imports disponibles: Mathlib.Algebra.Ring.Basic\n",
-    "Variables: (a b c : Nat)\n",
-    "\n",
-    "Théorème:\n",
-    "theorem distrib_example (a b c : Nat) : a * (b + c) = a * b + a * c := by sorry\n",
-    "\n",
-    "Utilise les tactiques Mathlib appropriees.\n",
-    "```\n",
-    "\n",
-    "#### 2. Prompt de correction : Feedback cible\n",
-    "\n",
-    "Quand une preuve echoue, le prompt de correction doit :\n",
-    "- Montrer le code qui a echoue\n",
-    "- Inclure l'erreur Lean complète (ligne, message)\n",
-    "- Demander une correction SPÉCIFIQUE\n",
-    "\n",
-    "**Itération typique** :\n",
-    "1. LLM suggere `by rfl`\n",
-    "2. Lean repond `type mismatch`\n",
-    "3. Correction : `by omega` ou `by ring`\n",
-    "\n",
-    "#### 3. Few-shot learning : Exemples similaires\n",
-    "\n",
-    "Fournir 2-3 exemples de preuves similaires ameliore drastiquement les résultats :\n",
-    "\n",
-    "```\n",
-    "Exemple 1:\n",
-    "theorem add_comm (a b : Nat) : a + b = b + a := by\n",
-    "  exact Nat.add_comm a b\n",
-    "\n",
-    "Exemple 2:\n",
-    "theorem mul_comm (a b : Nat) : a * b = b * a := by\n",
-    "  exact Nat.mul_comm a b\n",
-    "\n",
-    "Maintenant prouvé:\n",
-    "theorem add_mul_comm (a b c : Nat) : (a + b) * c = a * c + b * c\n",
-    "```\n",
-    "\n",
-    "#### 4. Temperature et determinisme\n",
-    "\n",
-    "| Temperature | Comportement | Usage |\n",
-    "|-------------|--------------|-------|\n",
-    "| 0.0-0.3 | Déterministe, predictible | Preuves simples, tactiques standard |\n",
-    "| 0.4-0.7 | Creatif, exploratoire | Preuves complexes, stratégies nouvelles |\n",
-    "| 0.8-1.0 | Très creatif, variable | Brainstorming, exploration |\n",
-    "\n",
-    "Pour Lean, **temperature 0.2-0.4** est optimale : assez déterministe pour eviter les erreurs syntaxiques, assez flexible pour trouver des solutions elegantes."
+    "### 6.4 Explications : Prompt Engineering pour Lean\n\nLe prompting efficace pour Lean necessite precision et structure. Voici les patterns cles :\n\n#### 1. Prompt initial : Contexte riche\n\nUn bon prompt initial inclut :\n- **Imports disponibles** : Mathlib, tactiques standard\n- **Variables et types** : `(a b : Nat)`, `(x : Real)`, etc.\n- **Hypotheses** : Lemmes et faits déjà etablis\n- **Théorème cible** : Formulation exacte\n\n**Exemple** :\n```\nImports disponibles: Mathlib.Algebra.Ring.Basic\nVariables: (a b c : Nat)\n\nThéorème:\ntheorem distrib_example (a b c : Nat) : a * (b + c) = a * b + a * c := by sorry\n\nUtilise les tactiques Mathlib appropriees.\n```\n\n#### 2. Prompt de correction : Feedback cible\n\nQuand une preuve echoue, le prompt de correction doit :\n- Montrer le code qui a echoue\n- Inclure l'erreur Lean complète (ligne, message)\n- Demander une correction SPÉCIFIQUE\n\n**Itération typique** :\n1. LLM suggere `by rfl`\n2. Lean repond `type mismatch`\n3. Correction : `by omega` ou `by ring`\n\n#### 3. Few-shot learning : Exemples similaires\n\nFournir 2-3 exemples de preuves similaires ameliore drastiquement les résultats :\n\n```\nExemple 1:\ntheorem add_comm (a b : Nat) : a + b = b + a := by\n  exact Nat.add_comm a b\n\nExemple 2:\ntheorem mul_comm (a b : Nat) : a * b = b * a := by\n  exact Nat.mul_comm a b\n\nMaintenant prouve:\ntheorem add_mul_comm (a b c : Nat) : (a + b) * c = a * c + b * c\n```\n\n#### 4. Temperature et determinisme\n\n| Temperature | Comportement | Usage |\n|-------------|--------------|-------|\n| 0.0-0.3 | Déterministe, predictible | Preuves simples, tactiques standard |\n| 0.4-0.7 | Creatif, exploratoire | Preuves complexes, stratégies nouvelles |\n| 0.8-1.0 | Très creatif, variable | Brainstorming, exploration |\n\nPour Lean, **temperature 0.2-0.4** est optimale : assez déterministe pour eviter les erreurs syntaxiques, assez flexible pour trouver des solutions elegantes."
    ]
   },
   {