feat(lean,#17888): greffe Sheydvasser Art 0/1 sur 2 cells pivots (Lean-6)

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-6-Mathlib-Essentials.ipynb

@@ -811,7 +811,13 @@
     "\n",
     "1. **Quand `ring` vs `omega`** : `ring` traite les *égalités polynomiales* (`(a+b)^2 = a^2 + 2ab + b^2`) ; `omega` traite les *inégalités et égalités linéaires* sur `Nat`/`Int`. Sur `x^2 = x*x`, `ring` réussit, `omega` échoue (non-linéaire). Sur `x + y = y + x`, les deux réussissent.\n",
     "2. **Limite** : `ring` ne sait PAS factoriser ou utiliser des hypothèses hétérogènes. Pour `(a+b)*(a-b) = a^2 - b^2`, `ring` réussit ; pour prouver ça *à partir de* `h1 : a^2 - b^2 = c`, il faut `linarith` ou du manuel.\n",
-    "3. **Pont** : Lean-12 (sensibilité) n'utilise presque jamais `ring` directement — ses égalités portent sur des sommes indicées et des normes, pas des polynômes plats. Mais `ring` sous-tend `simp` et `norm_num` qui, eux, apparaissent partout."
+    "3. **Pont** : Lean-12 (sensibilité) n'utilise presque jamais `ring` directement — ses égalités portent sur des sommes indicées et des normes, pas des polynômes plats. Mais `ring` sous-tend `simp` et `norm_num` qui, eux, apparaissent partout.",
+    "\n",
+    "\n",
+    "> **Pour aller plus loin — Surviving proofs, *Why Do We Care About Proofs?* (29/08/2026)**\n",
+    "> Sheydvasser, à l'article 0, insiste : une preuve n'est pas seulement un certificat, c'est une *stratégie* qui éclaire. Ici, le choix entre `ring` et `omega` n'est pas qu'une question de performance — c'est une décision *tactique* qui dépend du fragment d'arithmétique qu'on manipule (anneau commutatif clos vs arithmétique linéaire sur les entiers). Échec de l'un, succès de l'autre : c'est exactement le *réseau de concepts* qu'elle recommande d'expliciter, plutôt que de tester au hasard.\n",
+    "> *Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/why-do-we-care-about-proofs*\n",
+    "> *Archivé : G:\\Mon Drive\\MyIA\\IA\\Bibliographie IA\\Pedagogie-Proves\\Sheydvasser-Surviving-Proofs\\2026-08-29_why-do-we-care-about-proofs.html*"
    ]
   },
   {
@@ -4044,7 +4050,13 @@
     "3. **Tenter `rw?` / `simp?`** : pour les étapes de réécriture / simplification.\n",
     "4. **Si rien ne marche, chercher par nom** dans Moogle (recherche sémantique en langage naturel) ou Loogle (recherche par signature de type). Cf. cellules 38 et 40.\n",
     "\n",
-    "**Réflexe à transmettre** : avant de prouver manuellement une identité « évidente » (`a + b = b + a`, `0 + n = n`, `‖x + y‖ ≤ ‖x‖ + ‖y‖`), toujours tester si Mathlib n'a pas déjà le lemme. La majorité des preuves « from scratch » dans la partie haute (Lean-12+) réutilisent ~80 % de lemmes Mathlib, et ne *font* que la glue — exactement l'insight « state preconditions precisely; compose existing guarantees » de la grille de lecture Lean-3/4.\n"
+    "**Réflexe à transmettre** : avant de prouver manuellement une identité « évidente » (`a + b = b + a`, `0 + n = n`, `‖x + y‖ ≤ ‖x‖ + ‖y‖`), toujours tester si Mathlib n'a pas déjà le lemme. La majorité des preuves « from scratch » dans la partie haute (Lean-12+) réutilisent ~80 % de lemmes Mathlib, et ne *font* que la glue — exactement l'insight « state preconditions precisely; compose existing guarantees » de la grille de lecture Lean-3/4.\n",
+    "\n",
+    "\n",
+    "> **Pour aller plus loin — Surviving proofs, *The Importance of Understanding* (05/09/2026)**\n",
+    "> Sheydvasser, à l'article 1, recommande en principe 2 de *situer un énoncé dans son réseau de concepts*. La convention Mathlib `Namespace.Concept.property` qu'on présente ici (Semiring → Ring → CommRing → Field) est précisément la réalisation systématique de ce geste : un théorème n'est jamais isolé, il porte dans son nom les liens de généralisation et de spécialisation qui le rendent *lisible*. Le fait que `Nat.exists_infinite_primes` puisse se *reformuler* comme `Nat.Infinite : Set ℕ` puis comme `Nat.exists_infinite_primes` est exactement la généralisation qu'elle défend à l'article 1.\n",
+    "> *Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/the-importance-of-understanding*\n",
+    "> *Archivé : G:\\Mon Drive\\MyIA\\IA\\Bibliographie IA\\Pedagogie-Proves\\Sheydvasser-Surviving-Proofs\\2026-09-05_the-importance-of-understanding.html*"
    ]
   }
  ],