Skip to content

Commit d00a7c9

Browse files
jsboigeclaude
jsboige
and
claude
authored
fix(lean,#19730): re-executer Lean-37 Capstone Serre100 post-#19628 (#19918)
* 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 * fix(lean,#19730): recaler la prose du capstone Serre100 sur sa propre mesure Le dossier de domaine pose par myia-po-2027:CoursIA-2 (head 6986f3f) 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) <noreply@anthropic.com> --------- Co-authored-by: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
1 parent 9a80b78 commit d00a7c9

1 file changed

Lines changed: 107 additions & 85 deletions

File tree

‎MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb‎

Lines changed: 107 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@
55
"id": "752688e6",
66
"metadata": {
77
"papermill": {
8-
"duration": 0.003885,
9-
"end_time": "2026-09-25T09:21:11.930752",
8+
"duration": 0.001856,
9+
"end_time": "2026-10-08T11:02:10.940231+00:00",
1010
"exception": false,
11-
"start_time": "2026-09-25T09:21:11.926867",
11+
"start_time": "2026-10-08T11:02:10.938375+00:00",
1212
"status": "completed"
1313
},
1414
"tags": []
@@ -32,10 +32,10 @@
3232
"id": "94b1f321",
3333
"metadata": {
3434
"papermill": {
35-
"duration": 0.002235,
36-
"end_time": "2026-09-25T09:21:11.935711",
35+
"duration": 0.001356,
36+
"end_time": "2026-10-08T11:02:10.943131+00:00",
3737
"exception": false,
38-
"start_time": "2026-09-25T09:21:11.933476",
38+
"start_time": "2026-10-08T11:02:10.941775+00:00",
3939
"status": "completed"
4040
},
4141
"tags": []
@@ -60,18 +60,18 @@
6060
"id": "45c25256",
6161
"metadata": {
6262
"papermill": {
63-
"duration": 0.00199,
64-
"end_time": "2026-09-25T09:21:11.939702",
63+
"duration": 0.001424,
64+
"end_time": "2026-10-08T11:02:10.946134+00:00",
6565
"exception": false,
66-
"start_time": "2026-09-25T09:21:11.937712",
66+
"start_time": "2026-10-08T11:02:10.944710+00:00",
6767
"status": "completed"
6868
},
6969
"tags": []
7070
},
7171
"source": [
72-
"## 2. Où entrer : les huit carnets\n",
72+
"## 2. Où entrer : les quinze carnets\n",
7373
"\n",
74-
"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",
74+
"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",
7575
"\n",
7676
"| # | Carnet | Ce qu'il distille |\n",
7777
"|---|---|---|\n",
@@ -83,19 +83,26 @@
8383
"| 06 | [bulles diaboliques de Minkowski](Serre100/06-bulles-minkowski.ipynb) | la géométrie des nombres, calculée |\n",
8484
"| 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",
8585
"| 08 | [Serre dans Mathlib](Serre100/08-serre-dans-mathlib-Lean.ipynb) | le tour des cinq monuments de Serre présents dans Mathlib |\n",
86-
"\n",
87-
"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."
86+
"| 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",
87+
"| 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",
88+
"| 11 | [corps quadratiques imaginaires](Serre100/11-corps-quadratiques-reciprocite-quadratique.ipynb) | la réciprocité quadratique et les densités de Chebotarev |\n",
89+
"| 12 | [formes quadratiques binaires](Serre100/12-formes-quadratiques-binaires-nombre-classes.ipynb) | le nombre de classes des formes quadratiques binaires |\n",
90+
"| 13 | [loi de réciprocité quadratique II](Serre100/13-jacobi-kronecker-reciprocite-II.ipynb) | le symbole de Jacobi et le symbole de Kronecker |\n",
91+
"| 14 | [composition de Gauss](Serre100/14-formes-quadratiques-composition-gauss.ipynb) | la composition des formes quadratiques et le nombre de classes h(D) |\n",
92+
"| 15 | [quatre carrés de Lagrange](Serre100/15-quatre-carres-lagrange.ipynb) | tout entier est somme de quatre carrés |\n",
93+
"\n",
94+
"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."
8895
]
8996
},
9097
{
9198
"cell_type": "markdown",
9299
"id": "318cad0c",
93100
"metadata": {
94101
"papermill": {
95-
"duration": 0.001109,
96-
"end_time": "2026-09-25T09:21:11.942407",
102+
"duration": 0.001395,
103+
"end_time": "2026-10-08T11:02:10.949053+00:00",
97104
"exception": false,
98-
"start_time": "2026-09-25T09:21:11.941298",
105+
"start_time": "2026-10-08T11:02:10.947658+00:00",
99106
"status": "completed"
100107
},
101108
"tags": []
@@ -125,10 +132,10 @@
125132
"id": "abf1c43a",
126133
"metadata": {
127134
"papermill": {
128-
"duration": 0.001007,
129-
"end_time": "2026-09-25T09:21:11.945413",
135+
"duration": 0.001292,
136+
"end_time": "2026-10-08T11:02:10.951706+00:00",
130137
"exception": false,
131-
"start_time": "2026-09-25T09:21:11.944406",
138+
"start_time": "2026-10-08T11:02:10.950414+00:00",
132139
"status": "completed"
133140
},
134141
"tags": []
@@ -146,20 +153,20 @@
146153
"id": "6ff0b75f",
147154
"metadata": {
148155
"papermill": {
149-
"duration": 0.000933,
150-
"end_time": "2026-09-25T09:21:11.947345",
156+
"duration": 0.001666,
157+
"end_time": "2026-10-08T11:02:10.954920+00:00",
151158
"exception": false,
152-
"start_time": "2026-09-25T09:21:11.946412",
159+
"start_time": "2026-10-08T11:02:10.953254+00:00",
153160
"status": "completed"
154161
},
155162
"tags": []
156163
},
157164
"source": [
158165
"## 5. Mesurer la surface de la sous-série\n",
159166
"\n",
160-
"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",
167+
"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",
161168
"\n",
162-
"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."
169+
"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."
163170
]
164171
},
165172
{
@@ -168,16 +175,16 @@
168175
"id": "12a8b74d",
169176
"metadata": {
170177
"execution": {
171-
"iopub.execute_input": "2026-10-02T04:55:47.171949Z",
172-
"iopub.status.busy": "2026-10-02T04:55:47.171667Z",
173-
"iopub.status.idle": "2026-10-02T04:55:47.633481Z",
174-
"shell.execute_reply": "2026-10-02T04:55:47.632468Z"
178+
"iopub.execute_input": "2026-10-08T11:02:10.959058Z",
179+
"iopub.status.busy": "2026-10-08T11:02:10.958852Z",
180+
"iopub.status.idle": "2026-10-08T11:02:11.641179Z",
181+
"shell.execute_reply": "2026-10-08T11:02:11.640366Z"
175182
},
176183
"papermill": {
177-
"duration": 0.035154,
178-
"end_time": "2026-09-25T09:21:11.984113",
184+
"duration": 0.685815,
185+
"end_time": "2026-10-08T11:02:11.642310+00:00",
179186
"exception": false,
180-
"start_time": "2026-09-25T09:21:11.948959",
187+
"start_time": "2026-10-08T11:02:10.956495+00:00",
181188
"status": "completed"
182189
},
183190
"tags": []
@@ -187,7 +194,7 @@
187194
"name": "stdout",
188195
"output_type": "stream",
189196
"text": [
190-
"10 carnets dans Serre100/\n",
197+
"15 carnets dans Serre100/\n",
191198
"\n",
192199
"carnet kernel cells hors AST imports hors stdlib\n",
193200
"----------------------------------------------------------------------------------------------\n",
@@ -199,22 +206,25 @@
199206
]
200207
},
201208
{
202-
"name": "stderr",
209+
"name": "stdout",
203210
"output_type": "stream",
204211
"text": [
205-
"<unknown>:6: SyntaxWarning: invalid escape sequence '\\s'\n",
206-
"<unknown>:8: SyntaxWarning: invalid escape sequence '\\l'\n"
212+
"06-bulles-minkowski.ipynb python3 - matplotlib, numpy\n",
213+
"07-zeros-fonctions-l-gaps-gue.ipynb python3 - matplotlib\n",
214+
"08-serre-dans-mathlib-Lean.ipynb lean4-wsl 14 aucun\n",
215+
"09-congruences-tau-lacunarite-delta.ipynb python3 - matplotlib\n"
207216
]
208217
},
209218
{
210219
"name": "stdout",
211220
"output_type": "stream",
212221
"text": [
213-
"06-bulles-minkowski.ipynb python3 - matplotlib, numpy\n",
214-
"07-zeros-fonctions-l-gaps-gue.ipynb python3 - matplotlib\n",
215-
"08-serre-dans-mathlib.ipynb lean4-wsl 14 aucun\n",
216-
"09-congruences-tau-lacunarite-delta.ipynb python3 - matplotlib\n",
217222
"10-empilements-borne-lp-cohn-elkies.ipynb python3 - matplotlib, numpy, scipy\n",
223+
"11-corps-quadratiques-reciprocite-quadratique.ipynb python3 - aucun\n",
224+
"12-formes-quadratiques-binaires-nombre-classes.ipynb python3 - aucun\n",
225+
"13-jacobi-kronecker-reciprocite-II.ipynb python3 - aucun\n",
226+
"14-formes-quadratiques-composition-gauss.ipynb python3 - aucun\n",
227+
"15-quatre-carres-lagrange.ipynb python3 - aucun\n",
218228
"\n",
219229
"Dependances externes de toute la sous-serie : matplotlib, mpl_toolkits, numpy, scipy\n"
220230
]
@@ -285,33 +295,33 @@
285295
"id": "b74a13ea",
286296
"metadata": {
287297
"papermill": {
288-
"duration": 0.001615,
289-
"end_time": "2026-09-25T09:21:11.987773",
298+
"duration": 0.001667,
299+
"end_time": "2026-10-08T11:02:11.645834+00:00",
290300
"exception": false,
291-
"start_time": "2026-09-25T09:21:11.986158",
301+
"start_time": "2026-10-08T11:02:11.644167+00:00",
292302
"status": "completed"
293303
},
294304
"tags": []
295305
},
296306
"source": [
297307
"La mesure confirme le diptyque et **précise** la convention déclarée :\n",
298308
"\n",
299-
"- **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",
300-
"- La sous-série est bien **portée par la bibliothèque standard** : aucune dépendance de calcul n'apparaît.\n",
301-
"- 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",
309+
"- **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",
310+
"- 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",
311+
"- 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",
302312
"\n",
303-
"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."
313+
"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."
304314
]
305315
},
306316
{
307317
"cell_type": "markdown",
308318
"id": "504a93a2",
309319
"metadata": {
310320
"papermill": {
311-
"duration": 0.0018,
312-
"end_time": "2026-09-25T09:21:11.990681",
321+
"duration": 0.001635,
322+
"end_time": "2026-10-08T11:02:11.649194+00:00",
313323
"exception": false,
314-
"start_time": "2026-09-25T09:21:11.988881",
324+
"start_time": "2026-10-08T11:02:11.647559+00:00",
315325
"status": "completed"
316326
},
317327
"tags": []
@@ -327,10 +337,10 @@
327337
"id": "0947538b",
328338
"metadata": {
329339
"papermill": {
330-
"duration": 0.002015,
331-
"end_time": "2026-09-25T09:21:11.993665",
340+
"duration": 0.001626,
341+
"end_time": "2026-10-08T11:02:11.652436+00:00",
332342
"exception": false,
333-
"start_time": "2026-09-25T09:21:11.991650",
343+
"start_time": "2026-10-08T11:02:11.650810+00:00",
334344
"status": "completed"
335345
},
336346
"tags": []
@@ -351,16 +361,16 @@
351361
"id": "84387dc6",
352362
"metadata": {
353363
"execution": {
354-
"iopub.execute_input": "2026-10-02T04:55:47.637031Z",
355-
"iopub.status.busy": "2026-10-02T04:55:47.636759Z",
356-
"iopub.status.idle": "2026-10-02T04:55:47.641716Z",
357-
"shell.execute_reply": "2026-10-02T04:55:47.640659Z"
364+
"iopub.execute_input": "2026-10-08T11:02:11.656889Z",
365+
"iopub.status.busy": "2026-10-08T11:02:11.656452Z",
366+
"iopub.status.idle": "2026-10-08T11:02:11.661493Z",
367+
"shell.execute_reply": "2026-10-08T11:02:11.660773Z"
358368
},
359369
"papermill": {
360-
"duration": 0.005443,
361-
"end_time": "2026-09-25T09:21:12.000106",
370+
"duration": 0.00833,
371+
"end_time": "2026-10-08T11:02:11.662416+00:00",
362372
"exception": false,
363-
"start_time": "2026-09-25T09:21:11.994663",
373+
"start_time": "2026-10-08T11:02:11.654086+00:00",
364374
"status": "completed"
365375
},
366376
"tags": []
@@ -400,10 +410,10 @@
400410
"id": "64b5c7e0",
401411
"metadata": {
402412
"papermill": {
403-
"duration": 0.0,
404-
"end_time": "2026-09-25T09:21:12.002659",
413+
"duration": 0.002037,
414+
"end_time": "2026-10-08T11:02:11.666253+00:00",
405415
"exception": false,
406-
"start_time": "2026-09-25T09:21:12.002659",
416+
"start_time": "2026-10-08T11:02:11.664216+00:00",
407417
"status": "completed"
408418
},
409419
"tags": []
@@ -424,16 +434,16 @@
424434
"id": "1ee0d93f",
425435
"metadata": {
426436
"execution": {
427-
"iopub.execute_input": "2026-10-02T04:55:47.644979Z",
428-
"iopub.status.busy": "2026-10-02T04:55:47.644754Z",
429-
"iopub.status.idle": "2026-10-02T04:55:47.649547Z",
430-
"shell.execute_reply": "2026-10-02T04:55:47.648210Z"
437+
"iopub.execute_input": "2026-10-08T11:02:11.671190Z",
438+
"iopub.status.busy": "2026-10-08T11:02:11.670899Z",
439+
"iopub.status.idle": "2026-10-08T11:02:11.674761Z",
440+
"shell.execute_reply": "2026-10-08T11:02:11.673954Z"
431441
},
432442
"papermill": {
433-
"duration": 0.005001,
434-
"end_time": "2026-09-25T09:21:12.010341",
443+
"duration": 0.007353,
444+
"end_time": "2026-10-08T11:02:11.675620+00:00",
435445
"exception": false,
436-
"start_time": "2026-09-25T09:21:12.005340",
446+
"start_time": "2026-10-08T11:02:11.668267+00:00",
437447
"status": "completed"
438448
},
439449
"tags": []
@@ -467,10 +477,10 @@
467477
"id": "d2543d15",
468478
"metadata": {
469479
"papermill": {
470-
"duration": 0.001027,
471-
"end_time": "2026-09-25T09:21:12.013424",
480+
"duration": 0.001761,
481+
"end_time": "2026-10-08T11:02:11.679168+00:00",
472482
"exception": false,
473-
"start_time": "2026-09-25T09:21:12.012397",
483+
"start_time": "2026-10-08T11:02:11.677407+00:00",
474484
"status": "completed"
475485
},
476486
"tags": []
@@ -491,16 +501,16 @@
491501
"id": "0f5dbbff",
492502
"metadata": {
493503
"execution": {
494-
"iopub.execute_input": "2026-10-02T04:55:47.653123Z",
495-
"iopub.status.busy": "2026-10-02T04:55:47.652800Z",
496-
"iopub.status.idle": "2026-10-02T04:55:47.658208Z",
497-
"shell.execute_reply": "2026-10-02T04:55:47.656920Z"
504+
"iopub.execute_input": "2026-10-08T11:02:11.683533Z",
505+
"iopub.status.busy": "2026-10-08T11:02:11.683215Z",
506+
"iopub.status.idle": "2026-10-08T11:02:11.687697Z",
507+
"shell.execute_reply": "2026-10-08T11:02:11.687039Z"
498508
},
499509
"papermill": {
500-
"duration": 0.006044,
501-
"end_time": "2026-09-25T09:21:12.020729",
510+
"duration": 0.008043,
511+
"end_time": "2026-10-08T11:02:11.688864+00:00",
502512
"exception": false,
503-
"start_time": "2026-09-25T09:21:12.014685",
513+
"start_time": "2026-10-08T11:02:11.680821+00:00",
504514
"status": "completed"
505515
},
506516
"tags": []
@@ -535,10 +545,10 @@
535545
"id": "9bfe3694",
536546
"metadata": {
537547
"papermill": {
538-
"duration": 0.001638,
539-
"end_time": "2026-09-25T09:21:12.024894",
548+
"duration": 0.001715,
549+
"end_time": "2026-10-08T11:02:11.692590+00:00",
540550
"exception": false,
541-
"start_time": "2026-09-25T09:21:12.023256",
551+
"start_time": "2026-10-08T11:02:11.690875+00:00",
542552
"status": "completed"
543553
},
544554
"tags": []
@@ -548,9 +558,9 @@
548558
"\n",
549559
"Trois choses, dans cet ordre :\n",
550560
"\n",
551-
"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",
561+
"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",
552562
"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",
553-
"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",
563+
"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",
554564
"\n",
555565
"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",
556566
"\n",
@@ -574,7 +584,19 @@
574584
"name": "python",
575585
"nbconvert_exporter": "python",
576586
"pygments_lexer": "ipython3",
577-
"version": "3.13.15"
587+
"version": "3.13.3"
588+
},
589+
"papermill": {
590+
"default_parameters": {},
591+
"duration": 2.385164,
592+
"end_time": "2026-10-08T11:02:11.933472+00:00",
593+
"environment_variables": {},
594+
"exception": null,
595+
"input_path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb",
596+
"output_path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb",
597+
"parameters": {},
598+
"start_time": "2026-10-08T11:02:09.548308+00:00",
599+
"version": "2.7.0"
578600
}
579601
},
580602
"nbformat": 4,

0 commit comments

Comments
 (0)