diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb
index 16a8e28088..565a7d2996 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb
@@ -552,7 +552,7 @@
     "4. **Spécialisation** (irréductibilité de Hilbert) : de ℚ(t) vers le ℚ du polynôme f₁.\n",
     "\n",
     "Le dépôt porte déjà le socle géométrique de cette chaîne dans\n",
-    "[`grothendieck_lean`](grothendieck_lean/README.md) (34 modules, 0 sorry) : sites, faisceaux,\n",
+    "[`grothendieck_lean`](grothendieck_lean/README.md) (77 modules leaf + 1 umbrella Grothendieck.lean, 0 sorry ; 77 portent un sibling `_en` jumeau anglophone (couverture 1:1), verifie par `scripts/lean/check_grothendieck_readme.py`) : sites, faisceaux,\n",
     "cohomologie — mais **pas** le π₁ étale ni l'existence de Riemann. La phrase qui doit rester\n",
     "noir sur blanc : **« M₂₃ est un groupe de Galois sur ℚ » n'est PAS formalisé dans ce dépôt** —\n",
     "il est prouvé dans le préprint, et vérifié computationnellement ci-dessous au niveau du\n",