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..17f817a586 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,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", @@ -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." ] }, { @@ -92,10 +99,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 +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": [] @@ -146,10 +153,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": [] @@ -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." ] }, { @@ -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": [] @@ -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", @@ -199,22 +206,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 +295,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": [] @@ -296,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." ] }, { @@ -308,10 +318,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 +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": [] @@ -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": [] @@ -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": [] @@ -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": [] @@ -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": [] @@ -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": [] @@ -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": [] @@ -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", @@ -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,