From 6986f3f43ba7488aa4468828a57614ff17559b78 Mon Sep 17 00:00:00 2001 From: jsboige Date: Thu, 8 Oct 2026 13:02:49 +0200 Subject: [PATCH 1/2] fix(lean,#19730): re-executer Lean-37 Capstone Serre100 post-#19628 La PR #19628 (merge 10:42:38Z) elimine les SyntaxWarning de Serre100/01 en prefixant les chaines LaTeX par r. Le capstone Lean-37-Capstone- Serre100.ipynb n'avait pas ete re-execute par #19628 -- ses anciens outputs dataient du FileNotFoundError (cwd Papermill = worktree root au lieu de MyIA.AI.Notebooks/SymbolicAI/Lean/). Re-execution Papermill kernel `python3` (timeout 600s, cwd fixe via Stop & Repair regle 6 secrets-hygiene.md -- le notebook source est correct, c'est l'environnement d'exec qui etait mal positionne). Acceptance : - 0 SyntaxWarning sur les 4 cellules (verifie par ast.parse + warnings.catch_warnings, voir scratchpad check_syntax_warnings.py) - 4/4 cellules executees (exec_count 1..4, outputs C.2 reels) : - Cell 0 : table 15 carnets Serre100/ + kernel + imports hors stdlib - Cells 1,2,3 : stubs `return None` (C.1 conforme, exercices etudiant) Residu : check_equivalence.py rend LOST_OUTPUTS (16/23 lignes dans la page GH Pages, 7 carnet manquants). Cause : la page publiee contient la table a 8 carnets (etat historique), alors que la sous-serie en compte 15 aujourd'hui. La re-publication GH Pages est externe au repo (workflow Quarto sur branche gh-pages). La lane n'a pas la main -- acceptance finale deleguee au coord/adjoint. Refs #19628, #19581, #19730 --- .../Lean/Lean-37-Capstone-Serre100.ipynb | 163 ++++++++++-------- 1 file changed, 89 insertions(+), 74 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb index 02528eca28..55cad7c65e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb @@ -5,10 +5,10 @@ "id": "752688e6", "metadata": { "papermill": { - "duration": 0.003885, - "end_time": "2026-09-25T09:21:11.930752", + "duration": 0.001856, + "end_time": "2026-10-08T11:02:10.940231+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.926867", + "start_time": "2026-10-08T11:02:10.938375+00:00", "status": "completed" }, "tags": [] @@ -32,10 +32,10 @@ "id": "94b1f321", "metadata": { "papermill": { - "duration": 0.002235, - "end_time": "2026-09-25T09:21:11.935711", + "duration": 0.001356, + "end_time": "2026-10-08T11:02:10.943131+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.933476", + "start_time": "2026-10-08T11:02:10.941775+00:00", "status": "completed" }, "tags": [] @@ -60,10 +60,10 @@ "id": "45c25256", "metadata": { "papermill": { - "duration": 0.00199, - "end_time": "2026-09-25T09:21:11.939702", + "duration": 0.001424, + "end_time": "2026-10-08T11:02:10.946134+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.937712", + "start_time": "2026-10-08T11:02:10.944710+00:00", "status": "completed" }, "tags": [] @@ -92,10 +92,10 @@ "id": "318cad0c", "metadata": { "papermill": { - "duration": 0.001109, - "end_time": "2026-09-25T09:21:11.942407", + "duration": 0.001395, + "end_time": "2026-10-08T11:02:10.949053+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.941298", + "start_time": "2026-10-08T11:02:10.947658+00:00", "status": "completed" }, "tags": [] @@ -125,10 +125,10 @@ "id": "abf1c43a", "metadata": { "papermill": { - "duration": 0.001007, - "end_time": "2026-09-25T09:21:11.945413", + "duration": 0.001292, + "end_time": "2026-10-08T11:02:10.951706+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.944406", + "start_time": "2026-10-08T11:02:10.950414+00:00", "status": "completed" }, "tags": [] @@ -146,10 +146,10 @@ "id": "6ff0b75f", "metadata": { "papermill": { - "duration": 0.000933, - "end_time": "2026-09-25T09:21:11.947345", + "duration": 0.001666, + "end_time": "2026-10-08T11:02:10.954920+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.946412", + "start_time": "2026-10-08T11:02:10.953254+00:00", "status": "completed" }, "tags": [] @@ -168,16 +168,16 @@ "id": "12a8b74d", "metadata": { "execution": { - "iopub.execute_input": "2026-10-02T04:55:47.171949Z", - "iopub.status.busy": "2026-10-02T04:55:47.171667Z", - "iopub.status.idle": "2026-10-02T04:55:47.633481Z", - "shell.execute_reply": "2026-10-02T04:55:47.632468Z" + "iopub.execute_input": "2026-10-08T11:02:10.959058Z", + "iopub.status.busy": "2026-10-08T11:02:10.958852Z", + "iopub.status.idle": "2026-10-08T11:02:11.641179Z", + "shell.execute_reply": "2026-10-08T11:02:11.640366Z" }, "papermill": { - "duration": 0.035154, - "end_time": "2026-09-25T09:21:11.984113", + "duration": 0.685815, + "end_time": "2026-10-08T11:02:11.642310+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.948959", + "start_time": "2026-10-08T11:02:10.956495+00:00", "status": "completed" }, "tags": [] @@ -187,7 +187,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "10 carnets dans Serre100/\n", + "15 carnets dans Serre100/\n", "\n", "carnet kernel cells hors AST imports hors stdlib\n", "----------------------------------------------------------------------------------------------\n", @@ -199,22 +199,25 @@ ] }, { - "name": "stderr", + "name": "stdout", "output_type": "stream", "text": [ - ":6: SyntaxWarning: invalid escape sequence '\\s'\n", - ":8: SyntaxWarning: invalid escape sequence '\\l'\n" + "06-bulles-minkowski.ipynb python3 - matplotlib, numpy\n", + "07-zeros-fonctions-l-gaps-gue.ipynb python3 - matplotlib\n", + "08-serre-dans-mathlib-Lean.ipynb lean4-wsl 14 aucun\n", + "09-congruences-tau-lacunarite-delta.ipynb python3 - matplotlib\n" ] }, { "name": "stdout", "output_type": "stream", "text": [ - "06-bulles-minkowski.ipynb python3 - matplotlib, numpy\n", - "07-zeros-fonctions-l-gaps-gue.ipynb python3 - matplotlib\n", - "08-serre-dans-mathlib.ipynb lean4-wsl 14 aucun\n", - "09-congruences-tau-lacunarite-delta.ipynb python3 - matplotlib\n", "10-empilements-borne-lp-cohn-elkies.ipynb python3 - matplotlib, numpy, scipy\n", + "11-corps-quadratiques-reciprocite-quadratique.ipynb python3 - aucun\n", + "12-formes-quadratiques-binaires-nombre-classes.ipynb python3 - aucun\n", + "13-jacobi-kronecker-reciprocite-II.ipynb python3 - aucun\n", + "14-formes-quadratiques-composition-gauss.ipynb python3 - aucun\n", + "15-quatre-carres-lagrange.ipynb python3 - aucun\n", "\n", "Dependances externes de toute la sous-serie : matplotlib, mpl_toolkits, numpy, scipy\n" ] @@ -285,10 +288,10 @@ "id": "b74a13ea", "metadata": { "papermill": { - "duration": 0.001615, - "end_time": "2026-09-25T09:21:11.987773", + "duration": 0.001667, + "end_time": "2026-10-08T11:02:11.645834+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.986158", + "start_time": "2026-10-08T11:02:11.644167+00:00", "status": "completed" }, "tags": [] @@ -308,10 +311,10 @@ "id": "504a93a2", "metadata": { "papermill": { - "duration": 0.0018, - "end_time": "2026-09-25T09:21:11.990681", + "duration": 0.001635, + "end_time": "2026-10-08T11:02:11.649194+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.988881", + "start_time": "2026-10-08T11:02:11.647559+00:00", "status": "completed" }, "tags": [] @@ -327,10 +330,10 @@ "id": "0947538b", "metadata": { "papermill": { - "duration": 0.002015, - "end_time": "2026-09-25T09:21:11.993665", + "duration": 0.001626, + "end_time": "2026-10-08T11:02:11.652436+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.991650", + "start_time": "2026-10-08T11:02:11.650810+00:00", "status": "completed" }, "tags": [] @@ -351,16 +354,16 @@ "id": "84387dc6", "metadata": { "execution": { - "iopub.execute_input": "2026-10-02T04:55:47.637031Z", - "iopub.status.busy": "2026-10-02T04:55:47.636759Z", - "iopub.status.idle": "2026-10-02T04:55:47.641716Z", - "shell.execute_reply": "2026-10-02T04:55:47.640659Z" + "iopub.execute_input": "2026-10-08T11:02:11.656889Z", + "iopub.status.busy": "2026-10-08T11:02:11.656452Z", + "iopub.status.idle": "2026-10-08T11:02:11.661493Z", + "shell.execute_reply": "2026-10-08T11:02:11.660773Z" }, "papermill": { - "duration": 0.005443, - "end_time": "2026-09-25T09:21:12.000106", + "duration": 0.00833, + "end_time": "2026-10-08T11:02:11.662416+00:00", "exception": false, - "start_time": "2026-09-25T09:21:11.994663", + "start_time": "2026-10-08T11:02:11.654086+00:00", "status": "completed" }, "tags": [] @@ -400,10 +403,10 @@ "id": "64b5c7e0", "metadata": { "papermill": { - "duration": 0.0, - "end_time": "2026-09-25T09:21:12.002659", + "duration": 0.002037, + "end_time": "2026-10-08T11:02:11.666253+00:00", "exception": false, - "start_time": "2026-09-25T09:21:12.002659", + "start_time": "2026-10-08T11:02:11.664216+00:00", "status": "completed" }, "tags": [] @@ -424,16 +427,16 @@ "id": "1ee0d93f", "metadata": { "execution": { - "iopub.execute_input": "2026-10-02T04:55:47.644979Z", - "iopub.status.busy": "2026-10-02T04:55:47.644754Z", - "iopub.status.idle": "2026-10-02T04:55:47.649547Z", - "shell.execute_reply": "2026-10-02T04:55:47.648210Z" + "iopub.execute_input": "2026-10-08T11:02:11.671190Z", + "iopub.status.busy": "2026-10-08T11:02:11.670899Z", + "iopub.status.idle": "2026-10-08T11:02:11.674761Z", + "shell.execute_reply": "2026-10-08T11:02:11.673954Z" }, "papermill": { - "duration": 0.005001, - "end_time": "2026-09-25T09:21:12.010341", + "duration": 0.007353, + "end_time": "2026-10-08T11:02:11.675620+00:00", "exception": false, - "start_time": "2026-09-25T09:21:12.005340", + "start_time": "2026-10-08T11:02:11.668267+00:00", "status": "completed" }, "tags": [] @@ -467,10 +470,10 @@ "id": "d2543d15", "metadata": { "papermill": { - "duration": 0.001027, - "end_time": "2026-09-25T09:21:12.013424", + "duration": 0.001761, + "end_time": "2026-10-08T11:02:11.679168+00:00", "exception": false, - "start_time": "2026-09-25T09:21:12.012397", + "start_time": "2026-10-08T11:02:11.677407+00:00", "status": "completed" }, "tags": [] @@ -491,16 +494,16 @@ "id": "0f5dbbff", "metadata": { "execution": { - "iopub.execute_input": "2026-10-02T04:55:47.653123Z", - "iopub.status.busy": "2026-10-02T04:55:47.652800Z", - "iopub.status.idle": "2026-10-02T04:55:47.658208Z", - "shell.execute_reply": "2026-10-02T04:55:47.656920Z" + "iopub.execute_input": "2026-10-08T11:02:11.683533Z", + "iopub.status.busy": "2026-10-08T11:02:11.683215Z", + "iopub.status.idle": "2026-10-08T11:02:11.687697Z", + "shell.execute_reply": "2026-10-08T11:02:11.687039Z" }, "papermill": { - "duration": 0.006044, - "end_time": "2026-09-25T09:21:12.020729", + "duration": 0.008043, + "end_time": "2026-10-08T11:02:11.688864+00:00", "exception": false, - "start_time": "2026-09-25T09:21:12.014685", + "start_time": "2026-10-08T11:02:11.680821+00:00", "status": "completed" }, "tags": [] @@ -535,10 +538,10 @@ "id": "9bfe3694", "metadata": { "papermill": { - "duration": 0.001638, - "end_time": "2026-09-25T09:21:12.024894", + "duration": 0.001715, + "end_time": "2026-10-08T11:02:11.692590+00:00", "exception": false, - "start_time": "2026-09-25T09:21:12.023256", + "start_time": "2026-10-08T11:02:11.690875+00:00", "status": "completed" }, "tags": [] @@ -574,9 +577,21 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.13.15" + "version": "3.13.3" + }, + "papermill": { + "default_parameters": {}, + "duration": 2.385164, + "end_time": "2026-10-08T11:02:11.933472+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb", + "output_path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb", + "parameters": {}, + "start_time": "2026-10-08T11:02:09.548308+00:00", + "version": "2.7.0" } }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file From ca2e58b983172542188f12a12b3e6cfb98a0f68a Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 9 Oct 2026 07:34:17 +0200 Subject: [PATCH 2/2] fix(lean,#19730): recaler la prose du capstone Serre100 sur sa propre mesure MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le dossier de domaine pose par myia-po-2027:CoursIA-2 (head 6986f3f43b) a confronte la sortie de la cellule 6 (`15 carnets dans Serre100/`) a la prose qui la commente. La table de la section 2 s'arretait a 08 et cinq phrases de compte disaient encore « huit » : la PR avait regenere les sorties sans toucher les phrases, laissant le carnet moins coherent avec lui-meme qu'avant. Corrections, cellules markdown seules (2, 5, 7, 15) : - table de la section 2 completee (lignes 09 a 15 ; titres releves dans les carnets eux-memes, pas supposes) ; - « huit carnets » -> « quinze carnets » (cellules 2, 5, 15) ; - « Sept carnets sur huit » -> « Quatorze carnets sur quinze » (cellules 7, 15) ; - numpy : « deux carnets, 05 et 06 » -> trois carnets, 05, 06 et 10 ; - dependances externes : « matplotlib, numpy » -> matplotlib, mpl_toolkits, numpy, scipy ; commande d'installation recalee en consequence ; - « l'arithmetique reste en bibliotheque standard » : faux pour le carnet 10, ou `np.linalg`/`np.exp`/`np.sqrt` portent l'evaluation de la borne de Cohn-Elkies et `scipy.optimize.linprog` resout le programme lineaire. La phrase dit desormais que numpy n'entre dans un calcul qu'a ce carnet. Le controle negatif du dossier tient : la cellule 3 annonce cinq modules et sa table en porte cinq. Diff markdown seul : aucune cellule de code touchee, donc aucune re-execution due (C.2/C.3) ; les sorties commitees restent intactes. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Lean/Lean-37-Capstone-Serre100.ipynb | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb index 55cad7c65e..17f817a586 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb @@ -69,9 +69,9 @@ "tags": [] }, "source": [ - "## 2. Où entrer : les huit carnets\n", + "## 2. Où entrer : les quinze carnets\n", "\n", - "La sous-série vit dans le dossier [`Serre100/`](Serre100/README.md) — huit carnets, un README et le lake. Le tableau dit, par carnet, ce qu'il distille.\n", + "La sous-série vit dans le dossier [`Serre100/`](Serre100/README.md) — quinze carnets, un README et le lake. Le tableau dit, par carnet, ce qu'il distille.\n", "\n", "| # | Carnet | Ce qu'il distille |\n", "|---|---|---|\n", @@ -83,8 +83,15 @@ "| 06 | [bulles diaboliques de Minkowski](Serre100/06-bulles-minkowski.ipynb) | la géométrie des nombres, calculée |\n", "| 07 | [zéros de fonctions L, gaps et statistique GUE](Serre100/07-zeros-fonctions-l-gaps-gue.ipynb) | les zéros et leurs écarts, confrontés à la statistique GUE |\n", "| 08 | [Serre dans Mathlib](Serre100/08-serre-dans-mathlib-Lean.ipynb) | le tour des cinq monuments de Serre présents dans Mathlib |\n", - "\n", - "Sept carnets tournent sur le kernel `python3` ; le huitième exige le kernel Lean et le lake construit. La section 5 **mesure** cette répartition au lieu de la supposer." + "| 09 | [τ de Ramanujan](Serre100/09-congruences-tau-lacunarite-delta.ipynb) | les congruences de τ, la borne de Deligne, et la lacunarité qui s'arrête aux portes de Δ |\n", + "| 10 | [empilements de sphères](Serre100/10-empilements-borne-lp-cohn-elkies.ipynb) | la borne linéaire de Cohn–Elkies, évaluée par programmation linéaire |\n", + "| 11 | [corps quadratiques imaginaires](Serre100/11-corps-quadratiques-reciprocite-quadratique.ipynb) | la réciprocité quadratique et les densités de Chebotarev |\n", + "| 12 | [formes quadratiques binaires](Serre100/12-formes-quadratiques-binaires-nombre-classes.ipynb) | le nombre de classes des formes quadratiques binaires |\n", + "| 13 | [loi de réciprocité quadratique II](Serre100/13-jacobi-kronecker-reciprocite-II.ipynb) | le symbole de Jacobi et le symbole de Kronecker |\n", + "| 14 | [composition de Gauss](Serre100/14-formes-quadratiques-composition-gauss.ipynb) | la composition des formes quadratiques et le nombre de classes h(D) |\n", + "| 15 | [quatre carrés de Lagrange](Serre100/15-quatre-carres-lagrange.ipynb) | tout entier est somme de quatre carrés |\n", + "\n", + "Quatorze carnets tournent sur le kernel `python3` ; seul `08` exige le kernel Lean et le lake construit. La section 5 **mesure** cette répartition au lieu de la supposer." ] }, { @@ -157,9 +164,9 @@ "source": [ "## 5. Mesurer la surface de la sous-série\n", "\n", - "Un capstone sert à décider **si on entre**. La question concrète du lecteur — « qu'est-ce que je dois installer pour lire ces huit carnets ? » — a une réponse objective : elle est écrite dans les carnets eux-mêmes, sous forme d'importations.\n", + "Un capstone sert à décider **si on entre**. La question concrète du lecteur — « qu'est-ce que je dois installer pour lire ces quinze carnets ? » — a une réponse objective : elle est écrite dans les carnets eux-mêmes, sous forme d'importations.\n", "\n", - "La cellule suivante parcourt les huit carnets, classe leurs importations (stdlib / externe) et relève le kernel déclaré par chacun. Les cellules qu'`ast` ne peut pas lire — magics Jupyter, et surtout le code **Lean** du carnet 08 — sont **comptées et affichées**, jamais silencieusement ignorées : c'est ce compteur qui explique pourquoi 08 n'expose aucune importation Python." + "La cellule suivante parcourt les quinze carnets, classe leurs importations (stdlib / externe) et relève le kernel déclaré par chacun. Les cellules qu'`ast` ne peut pas lire — magics Jupyter, et surtout le code **Lean** du carnet 08 — sont **comptées et affichées**, jamais silencieusement ignorées : c'est ce compteur qui explique pourquoi 08 n'expose aucune importation Python." ] }, { @@ -299,11 +306,11 @@ "source": [ "La mesure confirme le diptyque et **précise** la convention déclarée :\n", "\n", - "- **Sept carnets sur huit** tournent sur `python3` — un seul (`08`) déclare le kernel `lean4-wsl`, et c'est précisément lui qui n'expose **aucune** importation Python : toutes ses cellules de code sont du Lean, donc hors de portée d'`ast`. Le compteur de cellules illisibles est ce qui rend ce « aucun » lisible comme du Lean, et non comme une absence de dépendance.\n", - "- La sous-série est bien **portée par la bibliothèque standard** : aucune dépendance de calcul n'apparaît.\n", - "- Mais la formule « aucune dépendance au-delà de matplotlib » est **imprécise** : `numpy` est importé par **deux** carnets, `05` et `06` — une seule cellule chacun. Dans les deux cas l'usage est **côté figure**, jamais côté arithmétique : en `05`, `np.array` construit les deux matrices passées à `imshow` (tables de caractères $S_3$ et $S_4$ en carte de chaleur) ; en `06`, `np.linspace`/`np.outer`/(`np.cos`, `np.sin`) maillent la sphère passée à `plot_surface`.\n", + "- **Quatorze carnets sur quinze** tournent sur `python3` — un seul (`08`) déclare le kernel `lean4-wsl`, et c'est précisément lui qui n'expose **aucune** importation Python : toutes ses cellules de code sont du Lean, donc hors de portée d'`ast`. Le compteur de cellules illisibles est ce qui rend ce « aucun » lisible comme du Lean, et non comme une absence de dépendance.\n", + "- La sous-série est **majoritairement portée par la bibliothèque standard** : douze carnets sur quinze n'importent, hors figures, aucune dépendance de calcul.\n", + "- Mais la formule « aucune dépendance au-delà de matplotlib » est **imprécise** : `numpy` est importé par **trois** carnets (`05`, `06` et `10`), et `scipy` par un seul (`10`). En `05` et `06` l'usage de `numpy` est **côté figure** — `np.array` construit les deux matrices passées à `imshow` en `05` (tables de caractères $S_3$ et $S_4$ en carte de chaleur) ; `np.linspace`/`np.outer`/`np.cos`/`np.sin` maillent la sphère passée à `plot_surface` en `06`. En `10`, il est **côté calcul** : `np.linalg`, `np.exp` et `np.sqrt` portent l'évaluation numérique de la borne de Cohn–Elkies, et `scipy.optimize.linprog` résout le programme linéaire qui la certifie.\n", "\n", - "Autrement dit : pour lire la sous-série, `pip install matplotlib numpy` suffit, et l'arithmétique des carnets ne dépend que de la stdlib. C'est la version **mesurée** de la convention — les exercices 1 et 2 la vérifient plus finement." + "Autrement dit : pour lire la sous-série, `pip install matplotlib numpy scipy` suffit (`mpl_toolkits` est fourni par `matplotlib`). Hors figures, douze carnets sur quinze ne dépendent que de la bibliothèque standard ; `numpy` n'entre dans un calcul qu'au carnet `10`, qui y joint `scipy`. C'est la version **mesurée** de la convention — les exercices 1 et 2 la vérifient plus finement." ] }, { @@ -551,9 +558,9 @@ "\n", "Trois choses, dans cet ordre :\n", "\n", - "1. **Un point d'entrée** : la sous-série Serre 100 est un diptyque de huit carnets, chacun rendant un énoncé de Serre calculable ; le dossier [`Serre100/`](Serre100/README.md) est son README.\n", + "1. **Un point d'entrée** : la sous-série Serre 100 est un diptyque de quinze carnets, chacun rendant un énoncé de Serre calculable ; le dossier [`Serre100/`](Serre100/README.md) est son README.\n", "2. **Un résultat formel cité** : le lake [`serre100_lean/`](Serre100/serre100_lean/) porte cinq modules FR et leurs miroirs `_en` — les noms cités en section 3 sont ceux des déclarations qui existent, et le carnet [08](Serre100/08-serre-dans-mathlib-Lean.ipynb) les fait tourner dans un noyau Lean réel.\n", - "3. **Une surface mesurée** : sept carnets sur `python3`, un sur `lean4-wsl` ; deux dépendances externes (`matplotlib`, `numpy`), toutes deux côté figure, l'arithmétique restant en bibliothèque standard.\n", + "3. **Une surface mesurée** : quatorze carnets sur `python3`, un sur `lean4-wsl` ; quatre dépendances externes (`matplotlib`, `mpl_toolkits`, `numpy`, `scipy`), dont `numpy` et `scipy` n'entrent dans un calcul qu'au carnet `10`.\n", "\n", "Cette forme — un capstone à la racine qui présente la sous-série et cite son lake, le dossier qui porte les carnets, le lake qui porte les preuves — est **l'escalier** que la série applique à ses sous-séries : le parcours principal garde une entrée explicite vers chacune, sans que le lecteur ait à en connaître l'existence par ailleurs.\n", "\n", @@ -594,4 +601,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +}