Skip to content

fix(lean,#19730): re-executer Lean-37 Capstone Serre100 post-#19628 #19918

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 2 commits into from
Oct 9, 2026
Merged

fix(lean,#19730): re-executer Lean-37 Capstone Serre100 post-#19628 #19918

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6986f3f
fix(lean,#19730): re-executer Lean-37 Capstone Serre100 post-#19628
jsboige Oct 8, 2026
ca2e58b
fix(lean,#19730): recaler la prose du capstone Serre100 sur sa propre…
jsboige Oct 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
192 changes: 107 additions & 85 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-37-Capstone-Serre100.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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": []
Expand All @@ -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": []
Expand All @@ -60,18 +60,18 @@
"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": []
},
"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",
Expand All @@ -83,19 +83,26 @@
"| 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."
]
},
{
"cell_type": "markdown",
"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": []
Expand Down Expand Up @@ -125,10 +132,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": []
Expand All @@ -146,20 +153,20 @@
"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": []
},
"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."
]
},
{
Expand All @@ -168,16 +175,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": []
Expand All @@ -187,7 +194,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",
Expand All @@ -199,22 +206,25 @@
]
},
{
"name": "stderr",
"name": "stdout",
"output_type": "stream",
"text": [
"<unknown>:6: SyntaxWarning: invalid escape sequence '\\s'\n",
"<unknown>: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"
]
Expand Down Expand Up @@ -285,33 +295,33 @@
"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": []
},
"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."
]
},
{
"cell_type": "markdown",
"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": []
Expand All @@ -327,10 +337,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": []
Expand All @@ -351,16 +361,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": []
Expand Down Expand Up @@ -400,10 +410,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": []
Expand All @@ -424,16 +434,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": []
Expand Down Expand Up @@ -467,10 +477,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": []
Expand All @@ -491,16 +501,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": []
Expand Down Expand Up @@ -535,10 +545,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": []
Expand All @@ -548,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",
Expand All @@ -574,7 +584,19 @@
"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,
Expand Down
Loading