jsboige · Nov 4, 2026 · Nov 4, 2026 · Nov 4, 2026 · Nov 4, 2026 · Nov 5, 2026
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08b-Erdos-Formal-Conjectures-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-08b-Erdos-Formal-Conjectures-Lean.ipynb
@@ -50,7 +50,10 @@
     "3. **Le pattern conjecture-as-sorry** — Erdős–Moser restatée, `sorryAx` visible.\n",
     "4. **Provenance, attribution, dépendances** — d'où vient chaque brique.\n",
     "5. **Friction et chemin de découverte** — ce qui a résisté.\n",
-    "6. **Exercices**.\n"
+    "6. **Exercices**.\n",
+    "\n",
+    "\n",
+    "**Comment lire ce carnet.** Les six premières sections sont des démonstrations déjà exécutées : chaque cellule de code y est suivie d'une lecture qui cite sa sortie commitée telle quelle. Rien à compléter avant la section 6.\n"
    ]
   },
   {
@@ -71,7 +74,13 @@
     "\n",
     "Notebook **natif** : kernel `lean4-wsl-groth16200` (pattern per-lake), miroir WSL du lake grothendieck, pin `v4.33.0`, oleans Mathlib chauds. Le lake se choisit **dans le kernelspec, pas dans le notebook**.\n",
     "\n",
-    "Contrainte du REPL mesurée sur les précédents natifs : les `import` ne commitent l'environnement **que seuls dans leur cellule** — mélangés à d'autres commandes, ils sont ignorés silencieusement. D'où la cellule suivante.\n"
+    "Contrainte du REPL mesurée sur les précédents natifs : les `import` ne commitent l'environnement **que seuls dans leur cellule** — mélangés à d'autres commandes, ils sont ignorés silencieusement. D'où la cellule suivante.\n",
+    "\n",
+    "\n",
+    "Le pin `v4.33.0` rend les lectures reproductibles : les signatures et les axiomes lus ci-dessous sont ceux de cette version de Mathlib, et une mise à jour pourrait renommer ou déplacer `Int.erdos_ginzburg_ziv`.\n",
+    "\n",
+    "\n",
+    "Les sorties de ce carnet ont un format bavard (`Raw input:` / `Raw output:`) : c'est le protocole du REPL lean4-wsl, qui échoue la commande JSON envoyée au noyau puis répond par `{\"env\": n}` — l'incrément d'environnement est la preuve que la commande a bien été exécutée et a produit un nouvel état du noyau.\n"
    ]
   },
   {
@@ -143,6 +152,14 @@
     "import Mathlib.Tactic\n"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "lecture-sortie-import",
+   "metadata": {},
+   "source": [
+    "**Lecture de la sortie.** Le bloc se termine par `Raw output:` puis `{\"env\": 0}` : le REPL a créé l'environnement 0 et y a compilé les deux `import` sans aucun diagnostic. `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` et `Mathlib.Tactic` sont chargés pour toutes les cellules suivantes.\n"
+   ]
+  },
   {
    "cell_type": "markdown",
    "id": "439b1b08",
@@ -161,7 +178,13 @@
     "\n",
     "**Énoncé** (1935) : toute suite d'au moins `2n − 1` entiers contient une sous-suite de `n` éléments dont la somme est divisible par `n`. C'est un pilier de la combinatoire additive — le terrain où Erdős a le plus semé.\n",
     "\n",
-    "Mathlib embarque ce théorème (`Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.lean`) en quatre variantes : `Int` (divisibilité), `ZMod` (somme nulle), et leurs déclinaisons `Multiset`. La preuve procède par induction sur la décomposition en facteurs premiers de `n`, le cas premier étant délégué en amont dans le même fichier.\n"
+    "Mathlib embarque ce théorème (`Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.lean`) en quatre variantes : `Int` (divisibilité), `ZMod` (somme nulle), et leurs déclinaisons `Multiset`. La preuve procède par induction sur la décomposition en facteurs premiers de `n`, le cas premier étant délégué en amont dans le même fichier.\n",
+    "\n",
+    "\n",
+    "Pourquoi EGZ est un bon candidat de digestion : la preuve originale tient en quelques pages, elle est entièrement vérifiée par le noyau dans Mathlib, et elle se réutilise telle quelle — digérer ce théorème, c'est le lire et l'appliquer, pas le redémontrer.\n",
+    "\n",
+    "\n",
+    "Les quatre variantes se répartissent selon deux axes : le type des entiers (`ℤ` avec divisibilité, ou `ZMod n` avec somme nulle) et le type de suite (`Finset ι` indexée, ou `Multiset`). La section 2 utilisera la variante `ZMod` sur `Multiset`.\n"
    ]
   },
   {
@@ -277,7 +300,10 @@
    "source": [
     "**Lecture des signatures.** Le `ι` est un type d'index arbitraire, `s : Finset ι` la suite, l'hypothèse `2 * n - 1 ≤ #s` le cardinal minimal, la conclusion une existence : un sous-ensemble `t` de taille `n` à somme divisible par `n` (variante `Int`) ou nulle dans `ZMod n`.\n",
     "\n",
-    "Premier geste de digestion : demander au noyau **ce sur quoi repose la preuve**.\n"
+    "Premier geste de digestion : demander au noyau **ce sur quoi repose la preuve**.\n",
+    "\n",
+    "\n",
+    "En notation Lean, `↑n ∣ ∑ i ∈ t, a i` se lit « n divise la somme » dans `ℤ` (variante `Int`), et la variante `ZMod n` conclut directement à une somme nulle : les deux signatures se lisent sur la même sortie de `#check`.\n"
    ]
   },
   {
@@ -373,7 +399,13 @@
     "tags": []
    },
    "source": [
-    "**Lecture des axiomes.** La sortie donne les trois axiomes standard de Mathlib : `propext`, `Classical.choice`, `Quot.sound`. `Classical.choice` dit que la preuve est non constructive — accepté et **whitelisté par nom explicite** dans la politique d'axiomes du dépôt, jamais par wildcard. Le point décisif : **pas de `sorryAx`**. Le certificat est complet — la preuve existe, le noyau l'a vérifiée, et ce qui reste ce sont des choix fondationnels assumés.\n"
+    "**Lecture des axiomes.** La sortie donne les trois axiomes standard de Mathlib : `propext`, `Classical.choice`, `Quot.sound`. `Classical.choice` dit que la preuve est non constructive — accepté et **whitelisté par nom explicite** dans la politique d'axiomes du dépôt, jamais par wildcard. Le point décisif : **pas de `sorryAx`**. Le certificat est complet — la preuve existe, le noyau l'a vérifiée, et ce qui reste ce sont des choix fondationnels assumés.\n",
+    "\n",
+    "\n",
+    "Rappel de ce que sont ces trois axiomes : `propext` (extensionalité des propositions), `Quot.sound` (correction des quotients) et `Classical.choice` (choix classique, qui rend la preuve non constructive). Ce sont les seuls axiomes admis hors logique dans la politique du dépôt.\n",
+    "\n",
+    "\n",
+    "La whitelist par nom explicite a un rôle d'audit : elle fige la liste des axiomes admis, de sorte que l'apparition de `sorryAx` — ou de tout axiome inattendu — soit visible immédiatement dans la sortie de `#print axioms`.\n"
    ]
   },
   {
@@ -394,7 +426,10 @@
     "\n",
     "EGZ est un énoncé d'**existence**. La digestion l'incarne sur un cas calculable : `n = 3`, la suite `(0, 1, 1, 2, 2)` dans `ZMod 3` — exactement `2·3 − 1 = 5` éléments.\n",
     "\n",
-    "Le témoin `{0, 1, 2}` est de cardinal 3 et de somme `0 + 1 + 2 = 3 ≡ 0 (mod 3)` :\n"
+    "Le témoin `{0, 1, 2}` est de cardinal 3 et de somme `0 + 1 + 2 = 3 ≡ 0 (mod 3)` :\n",
+    "\n",
+    "\n",
+    "Un **témoin** (witness) est la part calculatoire de l'existence : EGZ affirme qu'un sous-ensemble existe, la cellule en exhibe un et laisse `decide` vérifier l'arithmétique modulaire. Le noyau vérifie le calcul ; le théorème importé garantit que ce calcul suffit à chaque fois.\n"
    ]
   },
   {
@@ -468,19 +503,10 @@
   },
   {
    "cell_type": "markdown",
-   "id": "435f7429",
-   "metadata": {
-    "papermill": {
-     "duration": 0.003404,
-     "end_time": "2026-09-17T15:00:43.823765+00:00",
-     "exception": false,
-     "start_time": "2026-09-17T15:00:43.820361+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
+   "id": "lecture-sortie-temoin",
+   "metadata": {},
    "source": [
-    "Et l'énoncé d'existence s'applique mécaniquement — Mathlib fournit le théorème, on fournit le cardinal :\n"
+    "**Lecture de la sortie.** Aucun avertissement : le REPL passe simplement à l'environnement suivant (`Raw output:` puis `{\"env\": 3}`). Cela signifie que `decide` a fermé le but — le témoin `{0, 1, 2}` a bien une somme nulle dans `ZMod 3`, vérifiée par calcul et non par import.\n"
    ]
   },
   {
@@ -569,7 +595,11 @@
     "tags": []
    },
    "source": [
-    "**Ce que cette paire de cellules montre** : l'existence certifiée (deuxième cellule) et le témoin concret vérifié (première cellule) sont deux choses distinctes. Nous n'avons **pas rejoué la preuve d'EGZ** — c'est l'import qui certifie ; la digestion relie l'énoncé importé au cas calculé.\n"
+    "Et l'énoncé d'existence s'applique mécaniquement — Mathlib fournit le théorème, on fournit le cardinal :\n",
+    "\n",
+    "**Ce que cette paire de cellules montre** : l'existence certifiée (deuxième cellule) et le témoin concret vérifié (première cellule) sont deux choses distinctes. Nous n'avons **pas rejoué la preuve d'EGZ** — c'est l'import qui certifie ; la digestion relie l'énoncé importé au cas calculé.\n",
+    "\n",
+    "**Lecture de la seconde sortie.** Aucun diagnostic, seulement `{\"env\": 4}` : `ZMod.erdos_ginzburg_ziv_multiset _ (by decide)` a été accepté, le noyau ayant vérifié lui-même par `decide` l'hypothèse de cardinal `2 * 3 - 1 ≤ 5`.\n"
    ]
   },
   {
@@ -590,7 +620,10 @@
     "\n",
     "L'équation `1^k + 2^k + ... + m^k = (m+1)^k`. Pour `k = 1` elle admet la solution triviale `1 + 2 = 3` (et elle seule) ; pour `k ≥ 2`, **personne ne sait** — aucun contre-exemple, aucune preuve, d'énormes bornes computationnelles (répertoriée dans la base [erdosproblems.com](https://www.erdosproblems.com/) et chez [Wikipedia](https://en.wikipedia.org/wiki/Erd%C5%91s%E2%80%93Moser_equation)).\n",
     "\n",
-    "Formalisée en Lean, une conjecture ouverte s'écrit **exactement comme un théorème** — au sorry près :\n"
+    "Formalisée en Lean, une conjecture ouverte s'écrit **exactement comme un théorème** — au sorry près :\n",
+    "\n",
+    "\n",
+    "Le pattern consiste à écrire la conjecture avec la syntaxe exacte d'un théorème, la preuve étant remplacée par `sorry`, puis à laisser `#print axioms` faire le tri : tout énoncé qui dépend de `sorryAx` est un énoncé non démontré, et cette dépendance se lit mécaniquement, sans inspecter la preuve.\n"
    ]
   },
   {
@@ -690,6 +723,14 @@
     "  sorry\n"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "lecture-sortie-sorry",
+   "metadata": {},
+   "source": [
+    "**Lecture de la sortie.** Le noyau répond par un avertissement « declaration uses `sorry` » : l'énoncé `erdos_moser_conjecture` est accepté, mais sa preuve est un trou délibéré. C'est le pattern **conjecture-as-sorry** : la conjecture est posée comme un théorème, et le `sorry` joue le rôle de ticket ouvert.\n"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 7,
@@ -769,6 +810,25 @@
     "#print axioms erdos_moser_conjecture\n"
    ]
   },
+  {
+   "cell_type": "markdown",
+   "id": "27585c79",
+   "metadata": {
+    "papermill": {
+     "duration": 0.003902,
+     "end_time": "2026-09-17T15:00:44.813607+00:00",
+     "exception": false,
+     "start_time": "2026-09-17T15:00:44.809705+00:00",
+     "status": "completed"
+    },
+    "tags": []
+   },
+   "source": [
+    "**Le discriminant, en une sortie** : `'erdos_moser_conjecture' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]`.\n",
+    "\n",
+    "Deux énoncés de forme syntaxique identique (`theorem ... := by ...`), et le noyau les sépare par leurs **axiomes** : la conjecture porte le trio standard **plus** `sorryAx` — c'est ce supplément qui dit que la preuve manque. C'est toute la mécanique du projet *formal-conjectures* : la base d'Erdős devient une collection d'énoncés `theorem ... := by sorry`, où chaque `sorry` est un **ticket ouvert**. Le benchmark du papier DeepMind mesure exactement la capacité d'un agent à faire tomber un `sorryAx` — le certificateur n'étant pas l'agent mais le noyau.\n"
+   ]
+  },
   {
    "cell_type": "code",
    "execution_count": 8,
@@ -840,23 +900,12 @@
   },
   {
    "cell_type": "markdown",
-   "id": "27585c79",
-   "metadata": {
-    "papermill": {
-     "duration": 0.003902,
-     "end_time": "2026-09-17T15:00:44.813607+00:00",
-     "exception": false,
-     "start_time": "2026-09-17T15:00:44.809705+00:00",
-     "status": "completed"
-    },
-    "tags": []
-   },
+   "id": "lecture-sortie-cas-k1",
+   "metadata": {},
    "source": [
-    "**Le discriminant, en une sortie** : `'erdos_moser_conjecture' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]`.\n",
-    "\n",
-    "Deux énoncés de forme syntaxique identique (`theorem ... := by ...`), et le noyau les sépare par leurs **axiomes** : la conjecture porte le trio standard **plus** `sorryAx` — c'est ce supplément qui dit que la preuve manque. C'est toute la mécanique du projet *formal-conjectures* : la base d'Erdős devient une collection d'énoncés `theorem ... := by sorry`, où chaque `sorry` est un **ticket ouvert**. Le benchmark du papier DeepMind mesure exactement la capacité d'un agent à faire tomber un `sorryAx` — le certificateur n'étant pas l'agent mais le noyau.\n",
+    "La troisième cellule rappelle pourquoi l'hypothèse `2 ≤ k` est nécessaire : sans elle l'énoncé serait **faux**, puisque `1 + 2 = 3` (vérifié par `decide`). Un énoncé de conjecture mal borné est un faux ticket : il serait réfutable sans être intéressant.\n",
     "\n",
-    "La troisième cellule rappelle pourquoi l'hypothèse `2 ≤ k` est nécessaire : sans elle l'énoncé serait **faux**, puisque `1 + 2 = 3` (vérifié par `decide`). Un énoncé de conjecture mal borné est un faux ticket : il serait réfutable sans être intéressant.\n"
+    "**Lecture de la sortie.** Aucun diagnostic, seulement `{\"env\": 7}` : `decide` a calculé `(∑ i ∈ Finset.range 2, (i + 1) ^ 1) = (2 + 1) ^ 1`, c'est-à-dire `1 + 2 = 3`.\n"
    ]
   },
   {
@@ -882,7 +931,10 @@
     "| Conjecture Erdős–Moser | base erdosproblems.com (Bloom) ; projet *Google DeepMind Formal Conjectures* ([arXiv:2605.13171](https://arxiv.org/abs/2605.13171), Firsching et al. 2026) | énoncé seul, `sorryAx` |\n",
     "| Raccord corpus | [Lean-7b](Lean-07b-Examples-Python.ipynb)/[Lean-8](Lean-08-Agentic-Proving-Python.ipynb) (agents, claims Erdős ancrés en #15209) ; lake `discrepancy_lean` #12839 (Beck-Fiala restatée) ; [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) (sensitivity, Huang 2019) | — |\n",
     "\n",
-    "**Attribution honnête** : la formalisation de l'équation d'Erdős–Moser ci-dessus est une restatement **pédagogique locale** — le projet *formal-conjectures* maintient ses propres énoncés ; nous n'importons ni ne reproduisons leur travail. La preuve d'EGZ n'est pas de ce dépôt : Mathlib la porte, ce notebook la **consomme et l'expose**.\n"
+    "**Attribution honnête** : la formalisation de l'équation d'Erdős–Moser ci-dessus est une restatement **pédagogique locale** — le projet *formal-conjectures* maintient ses propres énoncés ; nous n'importons ni ne reproduisons leur travail. La preuve d'EGZ n'est pas de ce dépôt : Mathlib la porte, ce notebook la **consomme et l'expose**.\n",
+    "\n",
+    "\n",
+    "**Vérification reproductible.** Chaque ligne de ce tableau se re-vérifie dans ce carnet : la colonne « axiomes » sort des deux `#print axioms` (sections 1 et 3), et la version est celle du pin du kernelspec. Aucune affirmation ici ne repose sur une source externe non citée.\n"
    ]
   },
   {
@@ -903,7 +955,10 @@
     "\n",
     "- **Le nom nu échoue** : `#check erdos_ginzburg_ziv` rend `unknown constant` — les théorèmes vivent sous préfixe de namespace (`Int.`, `ZMod.`). Première sonde du smoke, premier réflexe à enseigner.\n",
     "- **L'agrégateur ne suffit pas** : le lake avait l'agrégateur `Mathlib` chaud, mais le module `ErdosGinzburgZiv` devait être construit explicitement (`lake build Mathlib.Combinatorics.Additive.ErdosGinzburgZiv`) avant le run — un import de feuille exige l'olean de la feuille.\n",
-    "- **Le lake se choisit avant le notebook** : kernelspec per-lake (`--cd` dans l'argv), pas de `%cd` fonctionnel.\n"
+    "- **Le lake se choisit avant le notebook** : kernelspec per-lake (`--cd` dans l'argv), pas de `%cd` fonctionnel.\n",
+    "\n",
+    "\n",
+    "Ces frictions sont consignées parce qu'elles sont reproductibles : un lecteur qui rejoue le carnet dans le même kernelspec les retrouvera à l'identique, et elles documentent les pièges du REPL natif plutôt que des bugs du notebook.\n"
    ]
   },
   {
@@ -920,7 +975,9 @@
     "tags": []
    },
    "source": [
-    "## 6. Exercices\n"
+    "## 6. Exercices\n",
+    "\n",
+    "Trois cellules à compléter vous-même : chacune porte un commentaire `TODO etudiant` et doit être modifiée avant de produire sa sortie définitive. Complétez-les, puis réexécutez le carnet de bout en bout — il reste exécutable tel quel dans l'état livré.\n"
    ]
   },
   {
@@ -1257,7 +1314,10 @@
     "\n",
     "**Raccord.** [Lean-7b](Lean-07b-Examples-Python.ipynb) génère des preuves, [Lean-8](Lean-08-Agentic-Proving-Python.ipynb) orchestre des agents : la base d'Erdős formalisée est le terrain où ces agents se mesurent — la boucle est bouclée. [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) montre l'autre bout de l'histoire : une conjecture (sensitivity) devenue théorème, preuve de Huang 2019.\n",
     "\n",
-    "**Transmission.** Trois exercices exécutables, deux `#print axioms` à lire soi-même, et un critère à retenir : *le noyau ne lit pas les intentions, il lit les axiomes*.\n"
+    "**Transmission.** Trois exercices exécutables, deux `#print axioms` à lire soi-même, et un critère à retenir : *le noyau ne lit pas les intentions, il lit les axiomes*.\n",
+    "\n",
+    "\n",
+    "**Pour aller plus loin.** Le geste de ce carnet — formaliser une conjecture ouverte avec `sorry`, puis inspecter `#print axioms` — se généralise à toute la base erdosproblems.com : chaque problème y est suivi avec son statut de formalisation, et chaque `sorryAx` restant est un travail ouvert, lisible mécaniquement.\n"
    ]
   }
  ],