diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md index 598cf562f6..4487efbd9d 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md @@ -4,6 +4,8 @@ Sous-série de la série [Lean](../README.md) (décision de gradation #17545, 24 La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier porte l'arc d'analyse. Les numéros de la table ci-dessous renvoient à l'ancien identifiant de série (`Lean-18` → `ANALYSE-01`, etc. — table de correspondance dans `docs/reference/rename-ledger.tsv`). +**Escalier depuis la série principale** : [Lean-20 — Capstone](../Lean-20-Capstone-Digestions-Tao-Python.ipynb) présente la sous-série, en fait monter une première marche (règle de chaîne et distance de Ruzsa sur F₂³) et en mesure la surface. + | Carnet | Contenu | Durée | |---|---|---| | [ANALYSE-01-Sendov-Lean-Python](ANALYSE-01-Sendov-Lean-Python.ipynb) | La conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min | diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb new file mode 100644 index 0000000000..42113fb71d --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb @@ -0,0 +1,726 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "3ec1fd35", + "metadata": { + "papermill": { + "duration": 0.006113, + "end_time": "2026-09-29T14:04:24.348423", + "exception": false, + "start_time": "2026-09-29T14:04:24.342310", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# Lean-20 : Capstone — digérer le travail formel de Tao (sous-série ANALYSE)\n", + "\n", + "**Série** : [SymbolicAI / Lean](README.md) — escalier vers la sous-série [**ANALYSE**](ANALYSE/README.md)\n", + "\n", + "## Navigation\n", + "\n", + "| Notebook précédent | Notebook suivant |\n", + "|---|---|\n", + "| [Lean-17c - Knots Companion Formel](Lean-17c-Knots-Companion-Formel.ipynb) | [ANALYSE-01 - Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) pour entrer dans la sous-série, ou [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) pour poursuivre le parcours principal |\n", + "\n", + "***\n", + "\n", + "Ce capstone est **l'escalier** de la série Lean vers sa sous-série [**ANALYSE**](ANALYSE/README.md), qui occupe la place des anciens numéros 18 à 20b. Il fait trois choses. Il dit par où entrer et ce que la sous-série démontre. Il fait monter une première marche à la main : deux primitives de la preuve de PFR, calculées sur un petit groupe. Et il **mesure** la sous-série au lieu de la décrire.\n", + "\n", + "**Le fil de la sous-série n'est pas l'analyse, c'est la digestion.** Ses quatre carnets digèrent le travail formel de Terence Tao : la preuve de la conjecture de Sendov (L. Mazur, 2026), qu'il a digérée et formalisée ; son manuel *Analysis I*, écrit en Lean ; la conjecture PFR, prouvée avec T. Gowers, B. Green et F. Manners. Les deux premiers relèvent de l'analyse, pas les deux derniers : PFR est un théorème de combinatoire additive, prouvé par une méthode entropique. Les carnets se rangent d'ailleurs eux-mêmes sous « Digestions de résultats profonds », un nom plus juste que celui du dossier. Le nom du dossier est discuté dans l'issue [#18408](https://github.com/jsboige/CoursIA/issues/18408).\n", + "\n", + "**Prérequis** : le tutoriel de la série (numéros 1 à 6). **Durée** : 25 min. **Kernel** : `python3`, bibliothèque standard seule." + ] + }, + { + "cell_type": "markdown", + "id": "cc97422f", + "metadata": { + "papermill": { + "duration": 0.003522, + "end_time": "2026-09-29T14:04:24.359066", + "exception": false, + "start_time": "2026-09-29T14:04:24.355544", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. Le geste : digérer, pas seulement vérifier\n", + "\n", + "Tao distingue trois usages de l'IA sur les preuves : les **générer**, les **vérifier**, et les **digérer**, c'est-à-dire en tirer une compréhension. Sa déclaration *A Severe Misalignment of AI in Mathematics* (11 septembre 2026, DOI [10.5281/zenodo.22737750](https://doi.org/10.5281/zenodo.22737750)) rappelle la hiérarchie : *« Solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight. »*\n", + "\n", + "Une preuve vérifiée par Lean n'est pas encore une preuve comprise. La sous-série pratique la digestion à travers quatre gestes :\n", + "\n", + "| Geste | Ce qu'il produit | Où |\n", + "|---|---|---|\n", + "| **Lire** le lac | l'architecture de la preuve, fichier par fichier | ANALYSE-01, ANALYSE-02, ANALYSE-03 |\n", + "| **Raconter** | l'énoncé, ses cas, son contexte, dans une langue lisible | ANALYSE-01, ANALYSE-03 |\n", + "| **Extraire** | les primitives réutilisables hors du cadre d'origine | ANALYSE-04 |\n", + "| **Admettre** | l'endroit exact où une primitive cesse de valoir | ANALYSE-04 |\n", + "\n", + "Le dernier geste est celui qu'on oublie. Une primitive qui ne se transporte pas n'est pas un échec : c'est un résultat, qui dit où finit le cadre d'origine." + ] + }, + { + "cell_type": "markdown", + "id": "890e48d5", + "metadata": { + "papermill": { + "duration": 0.004459, + "end_time": "2026-09-29T14:04:24.367577", + "exception": false, + "start_time": "2026-09-29T14:04:24.363118", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Où entrer : les quatre carnets\n", + "\n", + "La sous-série vit dans le dossier [`ANALYSE/`](ANALYSE/README.md) : quatre carnets et un README.\n", + "\n", + "| # | Carnet | Ce qu'il digère | Lac source |\n", + "|---|---|---|---|\n", + "| 01 | [Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) | la conjecture de Sendov : si tous les zéros d'un polynôme sont dans le disque unité, chaque zéro a un point critique à distance au plus 1. Les cas du centre, de l'intérieur et du bord | `teorth/sendov` |\n", + "| 02 | [Analysis I](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | le manuel de Tao en Lean 4 : architecture du lac, auto-contenance face à Mathlib, cinq lemmes emblématiques | `teorth/analysis` |\n", + "| 03 | [PFR](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | la conjecture de Freiman-Ruzsa polynomiale sur F₂ⁿ et sa méthode entropique, avec des `#check` réels sur le lac compilé | `teorth/pfr` |\n", + "| 04 | [Primitives de PFR](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | trois primitives de la preuve, et l'endroit exact où chacune cesse de valoir | `teorth/pfr` |\n", + "\n", + "**Deux chemins de lecture.** 01 puis 02 apprennent à lire un lac de recherche. 03 puis 04 digèrent une preuve de recherche jusqu'à ses primitives. Le second chemin suppose l'entropie de Shannon : c'est la marche que la section 4 fait monter." + ] + }, + { + "cell_type": "markdown", + "id": "9aa81e9a", + "metadata": { + "papermill": { + "duration": 0.003787, + "end_time": "2026-09-29T14:04:24.375050", + "exception": false, + "start_time": "2026-09-29T14:04:24.371263", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Le versant formel : trois lacs externes\n", + "\n", + "Les carnets citent des déclarations réelles, pas des paraphrases. ANALYSE-03 passe à `#check`, dans un noyau Lean réel (`lean4-wsl`), les énoncés du lac `teorth/pfr` :\n", + "\n", + "- `PFR_conjecture`, la version combinatoire ;\n", + "- `entropic_PFR_conjecture`, la version entropique, formalisée en premier ;\n", + "- `rdist`, la distance entropique de Ruzsa ;\n", + "- `tau_strictly_decreases`, la descente stricte de la fonctionnelle τ qui fait avancer la preuve.\n", + "\n", + "ANALYSE-01 cite de même les modules du lac `teorth/sendov` (`Sendov.sendov`, `Sendov.sendov_center`, `Sendov.rubinstein_one`, entre autres). La section 5 compte ces citations dans les carnets au lieu de les recopier ici.\n", + "\n", + "ANALYSE-03 (section 1) donne la version entropique de PFR sous cette forme : pour deux variables X₁ et X₂ à valeurs dans F₂ⁿ, il existe un sous-groupe H tel que\n", + "\n", + "$$d[X_1 ; U_H] + d[X_2 ; U_H] \\le 11 \\cdot d[X_1 ; X_2],$$\n", + "\n", + "où U_H est la loi uniforme sur H et d la distance entropique de Ruzsa. Avec X₁ = X₂ = X, l'énoncé dit que **si X est presque « compressée » (d[X ; X] petit), alors X est proche d'une loi uniforme sur un sous-groupe**. C'est le sens de la formule « compression ⇒ structure »." + ] + }, + { + "cell_type": "markdown", + "id": "96d4e1f4", + "metadata": { + "papermill": { + "duration": 0.004533, + "end_time": "2026-09-29T14:04:24.384134", + "exception": false, + "start_time": "2026-09-29T14:04:24.379601", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. La marche : deux primitives de PFR à la main\n", + "\n", + "On travaille dans le plus petit groupe où l'énoncé a du sens, F₂³. Ses 8 éléments sont codés comme des entiers de 3 bits, et l'addition est le « ou exclusif » (XOR).\n", + "\n", + "- **Primitive 2 — projection et fibres.** Pour une projection π, par exemple le passage au quotient par un sous-groupe H, on a la règle de chaîne H(X) = H(π(X)) + H(X | π(X)). L'information de X se partage exactement entre la classe de X et sa position dans la fibre. La cellule prend H = {000, 001}, qui découpe F₂³ en 4 classes.\n", + "- **Primitive 1 — distance de Ruzsa.** d[X ; Y] = H(X' − Y') − H(X)/2 − H(Y)/2, où X' et Y' sont des copies indépendantes. Si X est uniforme sur un sous-groupe, X' − X'' est uniforme sur le même sous-groupe, donc d[X ; X] = 0. La cellule mélange la loi uniforme sur un sous-groupe à 4 éléments avec la loi uniforme sur F₂³, en proportion ε. Pour chaque mélange, elle cherche, parmi les 16 sous-groupes de F₂³, celui qui rend d[X ; U_H] minimal.\n", + "\n", + "*Copie pédagogique déclarée* : ces fonctions reprennent une petite partie d'ANALYSE-04 pour que la marche tienne en une cellule. La digestion complète, limites comprises, reste dans [ANALYSE-04](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb)." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "310ee90d", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-29T14:04:24.395149Z", + "iopub.status.busy": "2026-09-29T14:04:24.394634Z", + "iopub.status.idle": "2026-09-29T14:04:24.435863Z", + "shell.execute_reply": "2026-09-29T14:04:24.434217Z" + }, + "papermill": { + "duration": 0.048212, + "end_time": "2026-09-29T14:04:24.436901", + "exception": false, + "start_time": "2026-09-29T14:04:24.388689", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Primitive 2 -- regle de chaine H(X) = H(pi(X)) + H(X | pi(X))\n", + " H(X) = 2.708695 bits\n", + " H(pi(X)) = 1.760964 bits (4 classes)\n", + " H(X | pi(X)) = 0.947731 bits (moyenne sur les fibres)\n", + " ecart = 0.00e+00\n", + "\n", + "Primitive 1 -- distance de Ruzsa sur 16 sous-groupes de F_2^3\n", + " loi de X d[X;X] min_H d[X;U_H] |H*|\n", + " melange eps=0.0 0.0000 0.0000 4\n", + " melange eps=0.1 0.1665 0.1432 4\n", + " melange eps=0.3 0.2093 0.1951 8\n", + " melange eps=0.6 0.1002 0.0594 8\n", + " melange eps=1.0 0.0000 0.0000 8\n", + " X de la primitive 2 0.2520 0.1457 8\n" + ] + } + ], + "source": [ + "# Deux primitives de PFR, calculees a la main sur le groupe F_2^3.\n", + "# Copie pedagogique declaree : la digestion complete vit dans ANALYSE-04.\n", + "from itertools import combinations\n", + "from math import log2\n", + "\n", + "ELEMENTS = range(8) # F_2^3, un element = un entier de 3 bits, addition = XOR\n", + "\n", + "\n", + "def entropie(loi):\n", + " \"\"\"Entropie de Shannon (en bits) d'une loi {valeur: probabilite}.\"\"\"\n", + " return -sum(p * log2(p) for p in loi.values() if p > 0)\n", + "\n", + "\n", + "def loi_image(loi, f):\n", + " \"\"\"Loi de f(X) quand X suit `loi`.\"\"\"\n", + " image = {}\n", + " for x, p in loi.items():\n", + " image[f(x)] = image.get(f(x), 0.0) + p\n", + " return image\n", + "\n", + "\n", + "def entropie_conditionnelle(loi, f):\n", + " \"\"\"H(X | f(X)) : moyenne des entropies de X sur chaque fibre de f.\"\"\"\n", + " total = 0.0\n", + " for c, pc in loi_image(loi, f).items():\n", + " fibre = {x: p / pc for x, p in loi.items() if f(x) == c}\n", + " total += pc * entropie(fibre)\n", + " return total\n", + "\n", + "\n", + "def somme_independante(loi_x, loi_y):\n", + " \"\"\"Loi de X' - Y' pour des copies independantes (dans F_2^3, - = XOR).\"\"\"\n", + " somme = {}\n", + " for x, p in loi_x.items():\n", + " for y, q in loi_y.items():\n", + " somme[x ^ y] = somme.get(x ^ y, 0.0) + p * q\n", + " return somme\n", + "\n", + "\n", + "def distance_ruzsa(loi_x, loi_y):\n", + " \"\"\"Distance entropique de Ruzsa d[X ; Y] = H(X' - Y') - H(X)/2 - H(Y)/2.\"\"\"\n", + " return entropie(somme_independante(loi_x, loi_y)) - entropie(loi_x) / 2 - entropie(loi_y) / 2\n", + "\n", + "\n", + "def sous_groupes():\n", + " \"\"\"Les 16 sous-espaces de F_2^3, engendres par toutes les familles de vecteurs.\"\"\"\n", + " vus = set()\n", + " for k in range(4):\n", + " for famille in combinations(range(1, 8), k):\n", + " engendre = {0}\n", + " for v in famille:\n", + " engendre |= {x ^ v for x in engendre}\n", + " vus.add(frozenset(engendre))\n", + " return sorted(vus, key=lambda h: (len(h), sorted(h)))\n", + "\n", + "\n", + "def uniforme(ensemble):\n", + " return {x: 1 / len(ensemble) for x in ensemble}\n", + "\n", + "\n", + "# Primitive 2 : projection / fibres. Quotient par le sous-groupe H = {000, 001}.\n", + "X = {0: 0.30, 1: 0.20, 2: 0.15, 3: 0.05, 4: 0.10, 5: 0.10, 6: 0.05, 7: 0.05}\n", + "classe = lambda x: x & 0b110 # representant de la classe x + H\n", + "h_x = entropie(X)\n", + "h_pi = entropie(loi_image(X, classe))\n", + "h_fibres = entropie_conditionnelle(X, classe)\n", + "print(\"Primitive 2 -- regle de chaine H(X) = H(pi(X)) + H(X | pi(X))\")\n", + "print(\" H(X) = %.6f bits\" % h_x)\n", + "print(\" H(pi(X)) = %.6f bits (4 classes)\" % h_pi)\n", + "print(\" H(X | pi(X)) = %.6f bits (moyenne sur les fibres)\" % h_fibres)\n", + "print(\" ecart = %.2e\" % abs(h_x - (h_pi + h_fibres)))\n", + "\n", + "# Primitive 1 : distance de Ruzsa, et le signal compression => structure.\n", + "groupes = sous_groupes()\n", + "print(\"\\nPrimitive 1 -- distance de Ruzsa sur %d sous-groupes de F_2^3\" % len(groupes))\n", + "print(\" %-28s %10s %14s %8s\" % (\"loi de X\", \"d[X;X]\", \"min_H d[X;U_H]\", \"|H*|\"))\n", + "U_sg = uniforme({0, 1, 2, 3})\n", + "for eps in (0.0, 0.1, 0.3, 0.6, 1.0):\n", + " loi = {x: (1 - eps) * U_sg.get(x, 0.0) + eps / 8 for x in ELEMENTS}\n", + " d_xx = distance_ruzsa(loi, loi)\n", + " meilleur = min(groupes, key=lambda h: distance_ruzsa(loi, uniforme(h)))\n", + " d_xh = distance_ruzsa(loi, uniforme(meilleur))\n", + " print(\" %-28s %10.4f %14.4f %8d\" % (\"melange eps=%.1f\" % eps, d_xx, d_xh, len(meilleur)))\n", + "d_xx = distance_ruzsa(X, X)\n", + "meilleur = min(groupes, key=lambda h: distance_ruzsa(X, uniforme(h)))\n", + "print(\" %-28s %10.4f %14.4f %8d\" % (\"X de la primitive 2\", d_xx, distance_ruzsa(X, uniforme(meilleur)), len(meilleur)))" + ] + }, + { + "cell_type": "markdown", + "id": "aa3b2e24", + "metadata": { + "papermill": { + "duration": 0.003742, + "end_time": "2026-09-29T14:04:24.445384", + "exception": false, + "start_time": "2026-09-29T14:04:24.441642", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "- **La règle de chaîne tient exactement** : 2,7087 = 1,7610 + 0,9477 bits, avec un écart nul à la précision machine. Elle vaut pour toute loi et pour toute projection. C'est pourquoi ANALYSE-04 classe cette primitive parmi celles qui se transportent le plus largement.\n", + "- **La structure, c'est une distance nulle.** Aux deux extrémités, ε = 0 (loi uniforme sur un sous-groupe à 4 éléments) et ε = 1 (loi uniforme sur F₂³ tout entier, qui est lui-même un sous-groupe), d[X ; X] vaut exactement 0. Entre les deux, la distance est strictement positive, et le sous-groupe le plus proche passe de 4 à 8 éléments entre ε = 0,1 et ε = 0,3.\n", + "- **Sur chaque ligne, min_H d[X ; U_H] reste inférieur à d[X ; X]**, donc très en deçà de ce que garantit le théorème (2 · d[X ; U_H] ≤ 11 · d[X ; X]). Sur un groupe aussi petit, la borne n'est pas serrée, et on peut essayer les 16 sous-groupes un par un. Tout l'intérêt du théorème est qu'il vaut dans F₂ⁿ pour tout n, là où le nombre de sous-groupes explose et où aucune énumération n'est possible." + ] + }, + { + "cell_type": "markdown", + "id": "8026bf22", + "metadata": { + "papermill": { + "duration": 0.003769, + "end_time": "2026-09-29T14:04:24.453674", + "exception": false, + "start_time": "2026-09-29T14:04:24.449905", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Mesurer la surface de la sous-série\n", + "\n", + "Un capstone sert à décider **si l'on entre**. Les questions du lecteur (quel noyau, combien d'exercices, quels lacs) ont des réponses objectives, écrites dans les carnets eux-mêmes. La cellule suivante lit les quatre carnets. Pour chacun, elle relève :\n", + "\n", + "- le noyau déclaré ;\n", + "- le nombre de cellules de code et combien portent une trace d'exécution ;\n", + "- le nombre de titres d'exercice ;\n", + "- le nombre de déclarations distinctes passées à `#check` ;\n", + "- les lacs `teorth` cités ;\n", + "- le premier titre.\n", + "\n", + "Elle rend aussi visible ce que la description ne dit pas." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "a3afbf86", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-29T14:04:24.463650Z", + "iopub.status.busy": "2026-09-29T14:04:24.463100Z", + "iopub.status.idle": "2026-09-29T14:04:24.543336Z", + "shell.execute_reply": "2026-09-29T14:04:24.541647Z" + }, + "papermill": { + "duration": 0.087046, + "end_time": "2026-09-29T14:04:24.544399", + "exception": false, + "start_time": "2026-09-29T14:04:24.457353", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "carnet kernel code exec exos #check\n", + "ANALYSE-01-Sendov-Lean-Python.ipynb python3 10 10 3 1\n", + "ANALYSE-02-Tao-Lean-Python.ipynb python3 9 9 3 1\n", + "ANALYSE-03-PFR-Lean.ipynb lean4-wsl 9 9 3 17\n", + "ANALYSE-04-PFR-Primitives-Python.ipynb python3 6 6 0 0\n", + "\n", + "Lacs externes cites : ['teorth/analysis', 'teorth/pfr', 'teorth/sendov']\n", + "\n", + "Premier titre de chaque carnet :\n", + " ANALYSE-01- -> Lean-18 : La Conjecture de Sendov (preuve L. Mazur, digestio\n", + " ANALYSE-02- -> Lean-19 : Le manuel *Analysis I* de T. Tao en Lean 4 (lac `t\n", + " ANALYSE-03- -> Lean-20 : La conjecture de Freiman-Ruzsa polynomiale (PFR) —\n", + " ANALYSE-04- -> Lean-20b : Trois primitives de PFR, et l'endroit exact où el\n" + ] + } + ], + "source": [ + "# Surface de la sous-serie : on lit les carnets, on ne suppose rien.\n", + "import json\n", + "import os\n", + "import re\n", + "\n", + "RACINE = \"ANALYSE\"\n", + "\n", + "\n", + "def fiche(chemin):\n", + " \"\"\"Kernel, cellules executees, exercices, lacs cites et titre d'un carnet.\"\"\"\n", + " with open(chemin, encoding=\"utf-8\") as f:\n", + " carnet = json.load(f)\n", + " cellules = carnet[\"cells\"]\n", + " code = [c for c in cellules if c[\"cell_type\"] == \"code\"]\n", + " texte = \"\\n\".join(\"\".join(c[\"source\"]) for c in cellules)\n", + " titre = next(\n", + " (ligne for c in cellules if c[\"cell_type\"] == \"markdown\"\n", + " for ligne in \"\".join(c[\"source\"]).splitlines() if ligne.startswith(\"# \")),\n", + " \"(aucun titre)\",\n", + " )\n", + " return {\n", + " \"kernel\": carnet[\"metadata\"].get(\"kernelspec\", {}).get(\"name\", \"?\"),\n", + " \"code\": len(code),\n", + " \"executees\": sum(1 for c in code if c.get(\"execution_count\") is not None),\n", + " \"exercices\": len(re.findall(r\"(?m)^#{3,4} *(?:[\\d.]+ *)?Exercice\\b\", texte)),\n", + " \"lacs\": sorted(set(re.findall(r\"teorth/[\\w-]+\", texte))),\n", + " \"checks\": len(set(re.findall(r\"#check\\s+@?([\\w.]+)\", texte))),\n", + " \"titre\": titre[2:62],\n", + " }\n", + "\n", + "\n", + "carnets = sorted(n for n in os.listdir(RACINE) if n.endswith(\".ipynb\"))\n", + "print(\"%-40s %-10s %6s %6s %5s %6s\" % (\"carnet\", \"kernel\", \"code\", \"exec\", \"exos\", \"#check\"))\n", + "fiches = {}\n", + "for nom in carnets:\n", + " f = fiches[nom] = fiche(os.path.join(RACINE, nom))\n", + " print(\"%-40s %-10s %6d %6d %5d %6d\" % (nom[:40], f[\"kernel\"], f[\"code\"], f[\"executees\"], f[\"exercices\"], f[\"checks\"]))\n", + "\n", + "print(\"\\nLacs externes cites :\", sorted({l for f in fiches.values() for l in f[\"lacs\"]}))\n", + "print(\"\\nPremier titre de chaque carnet :\")\n", + "for nom, f in fiches.items():\n", + " print(\" %-12s -> %s\" % (nom[:11], f[\"titre\"]))" + ] + }, + { + "cell_type": "markdown", + "id": "c6cbd048", + "metadata": { + "papermill": { + "duration": 0.004189, + "end_time": "2026-09-29T14:04:24.552795", + "exception": false, + "start_time": "2026-09-29T14:04:24.548606", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "- **Un seul carnet tourne dans un noyau Lean** : ANALYSE-03 (`lean4-wsl`), qui passe 17 déclarations distinctes à `#check`. Les trois autres sont en `python3`. ANALYSE-01 et ANALYSE-02 pilotent le lac depuis Python, et ANALYSE-04 ne l'appelle pas.\n", + "- **Toutes les cellules de code portent une trace d'exécution** (10/10, 9/9, 9/9, 6/6).\n", + "- **Trois exercices dans chacun des trois premiers carnets, aucun dans ANALYSE-04.** C'est un écart à la convention des trois exercices par carnet.\n", + "- **Trois lacs externes**, tous publiés par Tao : `teorth/sendov`, `teorth/analysis`, `teorth/pfr`.\n", + "- **Les titres disent encore `Lean-18`, `Lean-19`, `Lean-20` et `Lean-20b`.** La descente dans le dossier a déplacé les fichiers sans renommer leurs titres.\n", + "\n", + "Les deux derniers défauts, avec le nom du dossier, sont suivis dans l'issue [#18408](https://github.com/jsboige/CoursIA/issues/18408). Cette mesure s'appuie sur les carnets eux-mêmes : elle suivra leur correction sans qu'on ait à réécrire cette section." + ] + }, + { + "cell_type": "markdown", + "id": "57fa15f7", + "metadata": { + "papermill": { + "duration": 0.003298, + "end_time": "2026-09-29T14:04:24.560366", + "exception": false, + "start_time": "2026-09-29T14:04:24.557068", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. Exercices\n", + "\n", + "Les trois exercices prolongent la marche et la mesure. Les stubs ne contiennent aucune erreur volontaire : le carnet s'exécute de bout en bout, exercices non complétés compris." + ] + }, + { + "cell_type": "markdown", + "id": "7a202548", + "metadata": { + "papermill": { + "duration": 0.004409, + "end_time": "2026-09-29T14:04:24.568785", + "exception": false, + "start_time": "2026-09-29T14:04:24.564376", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 1 — la règle de chaîne pour un autre quotient\n", + "\n", + "La section 4 a vérifié la règle de chaîne pour le quotient par H = {000, 001}. Vérifier qu'elle tient aussi pour H₂ = {000, 110}, qui découpe F₂³ autrement.\n", + "\n", + "**Étapes** : (1) écrire la fonction qui rend un représentant de la classe x + H₂ ; (2) calculer H(π(X)) et H(X | π(X)) avec les fonctions de la section 4 ; (3) vérifier que l'écart à H(X) est nul.\n", + "\n", + "**Indice** : la classe de x modulo H₂ est {x, x ^ 0b110}. Son plus petit élément en est un représentant." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "6206f935", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-29T14:04:24.578328Z", + "iopub.status.busy": "2026-09-29T14:04:24.578328Z", + "iopub.status.idle": "2026-09-29T14:04:24.588868Z", + "shell.execute_reply": "2026-09-29T14:04:24.587379Z" + }, + "papermill": { + "duration": 0.016659, + "end_time": "2026-09-29T14:04:24.589919", + "exception": false, + "start_time": "2026-09-29T14:04:24.573260", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice 1 a completer : definir classe_h2, puis verifier la regle de chaine.\n" + ] + } + ], + "source": [ + "# Exercice 1 : la regle de chaine pour le quotient par H2 = {000, 110}.\n", + "\n", + "\n", + "def classe_h2(x):\n", + " \"\"\"Representant de la classe de x modulo H2 = {000, 110}.\"\"\"\n", + " # TODO etudiant : rendre le plus petit des deux elements x et x ^ 0b110.\n", + " return None\n", + "\n", + "\n", + "if classe_h2(0) is None:\n", + " print(\"Exercice 1 a completer : definir classe_h2, puis verifier la regle de chaine.\")\n", + "else:\n", + " ecart = entropie(X) - entropie(loi_image(X, classe_h2)) - entropie_conditionnelle(X, classe_h2)\n", + " print(\"Ecart de la regle de chaine pour H2 : %.2e\" % abs(ecart))" + ] + }, + { + "cell_type": "markdown", + "id": "90a5459b", + "metadata": { + "papermill": { + "duration": 0.003726, + "end_time": "2026-09-29T14:04:24.597363", + "exception": false, + "start_time": "2026-09-29T14:04:24.593637", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 2 — une classe latérale est aussi structurée qu'un sous-groupe\n", + "\n", + "Le théorème parle de loi uniforme sur un sous-groupe, mais translater X ne change rien à sa structure. Montrer numériquement que la distance de Ruzsa est invariante par translation : d[X + v ; Y] = d[X ; Y] pour tout v de F₂³. En déduire que la loi uniforme sur la classe latérale H + v a une distance nulle à elle-même.\n", + "\n", + "**Étapes** : (1) écrire `loi_translatee(loi, v)`, la loi de X + v ; (2) comparer d[X + v ; X + v] et d[X ; X] pour les 8 valeurs de v ; (3) calculer d[U ; U] pour U uniforme sur {100, 101, 110, 111}, qui est la classe de 100 modulo {000, 001, 010, 011}.\n", + "\n", + "**Indice** : dans F₂³, X + v s'écrit `x ^ v` élément par élément. La probabilité ne change pas, seule l'étiquette bouge." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "7a8d81da", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-29T14:04:24.608530Z", + "iopub.status.busy": "2026-09-29T14:04:24.607997Z", + "iopub.status.idle": "2026-09-29T14:04:24.619277Z", + "shell.execute_reply": "2026-09-29T14:04:24.618278Z" + }, + "papermill": { + "duration": 0.018279, + "end_time": "2026-09-29T14:04:24.620457", + "exception": false, + "start_time": "2026-09-29T14:04:24.602178", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice 2 a completer : definir loi_translatee, puis comparer les distances.\n" + ] + } + ], + "source": [ + "# Exercice 2 : invariance de la distance de Ruzsa par translation.\n", + "\n", + "\n", + "def loi_translatee(loi, v):\n", + " \"\"\"Loi de X + v quand X suit `loi` (dans F_2^3, + = XOR).\"\"\"\n", + " # TODO etudiant : rendre le dictionnaire {x ^ v: p}.\n", + " return None\n", + "\n", + "\n", + "if loi_translatee(X, 1) is None:\n", + " print(\"Exercice 2 a completer : definir loi_translatee, puis comparer les distances.\")\n", + "else:\n", + " for v in ELEMENTS:\n", + " Xv = loi_translatee(X, v)\n", + " print(\"v = %d : d[X+v ; X+v] = %.6f\" % (v, distance_ruzsa(Xv, Xv)))\n", + " classe_laterale = uniforme({4, 5, 6, 7})\n", + " print(\"d[U ; U] sur la classe laterale :\", distance_ruzsa(classe_laterale, classe_laterale))" + ] + }, + { + "cell_type": "markdown", + "id": "8fbeb4e5", + "metadata": { + "papermill": { + "duration": 0.004352, + "end_time": "2026-09-29T14:04:24.628649", + "exception": false, + "start_time": "2026-09-29T14:04:24.624297", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 3 — les titres attendus, calculés depuis les noms de fichier\n", + "\n", + "La mesure de la section 5 montre des titres restés sur l'ancien identifiant (`Lean-18`…). Écrire la fonction qui, pour chaque carnet du dossier, déduit son identifiant **du nom de fichier** (`ANALYSE-01`, `ANALYSE-02`…) et signale les carnets dont le premier titre ne commence pas par cet identifiant. C'est le contrôle qu'une descente en dossier devrait passer avant son merge.\n", + "\n", + "**Étapes** : (1) extraire l'identifiant du nom de fichier avec une expression régulière ; (2) reprendre le premier titre relevé par `fiche` ; (3) rendre la liste des couples `(carnet, titre actuel)` en écart.\n", + "\n", + "**Indice** : `re.match(r\"(ANALYSE-\\d+)\", nom)` isole l'identifiant, et `fiches[nom][\"titre\"]` donne le titre sans son `# `." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "51f9f632", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-29T14:04:24.637123Z", + "iopub.status.busy": "2026-09-29T14:04:24.637123Z", + "iopub.status.idle": "2026-09-29T14:04:24.650690Z", + "shell.execute_reply": "2026-09-29T14:04:24.649678Z" + }, + "papermill": { + "duration": 0.019271, + "end_time": "2026-09-29T14:04:24.651951", + "exception": false, + "start_time": "2026-09-29T14:04:24.632680", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice 3 a completer\n" + ] + } + ], + "source": [ + "# Exercice 3 : les carnets dont le titre ne porte pas l'identifiant du fichier.\n", + "\n", + "\n", + "def titres_en_ecart(fiches):\n", + " \"\"\"Liste des couples (carnet, titre actuel) dont le titre ne commence pas par l'identifiant.\"\"\"\n", + " # TODO etudiant : deduire l'identifiant du nom de fichier, le comparer au\n", + " # debut du titre, et rendre les couples en ecart.\n", + " return None\n", + "\n", + "\n", + "resultat = titres_en_ecart(fiches)\n", + "print(\"Exercice 3 a completer\" if resultat is None else resultat)" + ] + }, + { + "cell_type": "markdown", + "id": "f0e2fdf2", + "metadata": { + "papermill": { + "duration": 0.003498, + "end_time": "2026-09-29T14:04:24.659185", + "exception": false, + "start_time": "2026-09-29T14:04:24.655687", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 7. Conclusion — ce que ce capstone laisse au lecteur\n", + "\n", + "1. **Un point d'entrée.** La sous-série [ANALYSE](ANALYSE/README.md) digère le travail formel de Tao en quatre carnets. Deux chemins la traversent : apprendre à lire un lac (01, 02), et digérer une preuve jusqu'à ses primitives (03, 04).\n", + "2. **Un résultat formel cité.** Les déclarations nommées en section 3 existent dans les lacs `teorth/sendov` et `teorth/pfr`. ANALYSE-03 les fait passer par un noyau Lean réel.\n", + "3. **Une marche montée.** La règle de chaîne et la distance de Ruzsa, calculées sur F₂³, suffisent pour lire l'énoncé entropique de PFR : une distance nulle est une structure, et une petite distance est une structure approchée.\n", + "4. **Une surface mesurée, avec ses défauts.** Les titres, les exercices d'ANALYSE-04 et le nom du dossier sont suivis dans [#18408](https://github.com/jsboige/CoursIA/issues/18408).\n", + "\n", + "**Suite.** Entrer par [ANALYSE-01](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), ou poursuivre le parcours principal avec [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb). Ce dernier reprend les deux registres de la sous-série : des illustrations numériques, puis des `#check` réels sur un lac compilé. Les primitives entropiques de PFR ont aussi vocation à être greffées dans la série ICT ([#18405](https://github.com/jsboige/CoursIA/issues/18405))." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.10.11" + }, + "papermill": { + "default_parameters": {}, + "duration": 5.217777, + "end_time": "2026-09-29T14:04:25.106111", + "environment_variables": {}, + "exception": null, + "input_path": "Lean-20-Capstone-Digestions-Tao-Python.ipynb", + "output_path": "Lean-20-Capstone-Digestions-Tao-Python.ipynb", + "parameters": {}, + "start_time": "2026-09-29T14:04:19.888334", + "version": "2.6.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb index a5fd6f945c..916465a688 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb @@ -16,7 +16,7 @@ "source": [ "# Lean-21 : Detection MIMO par flips -- le seuil 2 log N sous preuve Lean\n", "\n", - "**Navigation** : [Index](README.md) | [Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", + "**Navigation** : [Index](README.md) | [<< Lean-20 (Capstone Tao)](Lean-20-Capstone-Digestions-Tao-Python.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", "\n", "Ce notebook presente le lake **`mimo_lean`** de ce depot (issue #10984) : le port\n", "formel de l'algorithme de detection MIMO par flips de coordonnées de\n", @@ -39,7 +39,7 @@ "`M·ε·φ(2) ≥ 2·log N − log log N`, `P(erreur ML) ≥ 1 − exp(−(2·log N − log log N))`\n", "(issues #11673, #11709).\n", "\n", - "Comme dans [Lean-20](ANALYSE/ANALYSE-03-PFR-Lean.ipynb), nous procedons en deux\n", + "Comme dans [ANALYSE-03 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb), nous procedons en deux\n", "registres : des **illustrations numeriques** (Python) qui montrent les phenomenes,\n", "puis des **`#check` reels** executes par `lake env lean` sur le lac compile --\n", "les enonces affiches sont ceux que le compilateur Lean 4 a verifies, pas des\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index e3c2e4e241..1bd2150245 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -142,10 +142,11 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | # | Notebook | Contenu | Durée | |---|----------|---------|-------| -| 18 | [ANALYSE-01-Sendov-Lean-Python](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) | Ouverture de la sous-série [ANALYSE](ANALYSE/README.md) (dossier `ANALYSE/`, gradation #17545) — la conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min | -| 19 | [ANALYSE-02-Tao-Lean-Python](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min | -| 20 | [ANALYSE-03-PFR-Lean](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min | -| 20b | [ANALYSE-04-PFR-Primitives-Python](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | +| 20 | [Lean-20-Capstone-Digestions-Tao-Python](Lean-20-Capstone-Digestions-Tao-Python.ipynb) | **Capstone (escalier)** vers la sous-série [ANALYSE](ANALYSE/README.md), qui digère le travail formel de T. Tao : les gestes de la digestion (lire, raconter, extraire, admettre), la table de routage des quatre carnets et de leurs lacs (`teorth/sendov`, `teorth/analysis`, `teorth/pfr`), la marche montée à la main (règle de chaîne et distance de Ruzsa sur F₂³, le signal « compression ⇒ structure » de PFR), et la surface de la sous-série mesurée plutôt que déclarée — kernel `python3`, 3 exercices | 25 min | +| ANALYSE-01 | [ANALYSE-01-Sendov-Lean-Python](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) | Ouverture de la sous-série [ANALYSE](ANALYSE/README.md) (dossier `ANALYSE/`, gradation #17545) — la conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques des cas, contexte de la preuve | 45 min | +| ANALYSE-02 | [ANALYSE-02-Tao-Lean-Python](ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb) | Le manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 40 min | +| ANALYSE-03 | [ANALYSE-03-PFR-Lean](ANALYSE/ANALYSE-03-PFR-Lean.ipynb) | La conjecture PFR (polynomial Freiman–Ruzsa, ZMod 2) : méthode entropique de la preuve `teorth/pfr` — énoncé combinatoire, illustrations cosets dans F₂³, `#check` réels et axiomes du lac compilé | 45 min | +| ANALYSE-04 | [ANALYSE-04-PFR-Primitives-Python](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | | 21 | [Lean-21-MIMO-Detection-Flips](Lean-21-MIMO-Detection-Flips.ipynb) | Détection MIMO par flips de coordonnées (Papailiopoulos 2026) : le seuil 2·log N — descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo vs `e^{−np}`), `#check` réels des quatre phases et du converse complet `ml_error_prob_ge_threshold` (P(erreur ML) ≥ 1 − e^{−(2·log N − log log N)}) du companion `mimo_lean` (sorry-free, lake externe SLT pour Hanson–Wright) | 45 min | | 21b | [Lean-21b-MIMO-Converse-Native](Lean-21b-MIMO-Converse-Native.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lac `mimo_lean` : le lac importé et exécuté dans un kernel Lean 4 réel — la frontière SLT exhibée par `#check` (ce qui est prouvé vs emprunté à `YuanheZ/lean-stat-learning-theory`), les six déclarations de `NormTails` (concentration de Lipschitz gaussienne), les seize briques du converse Hanson–Wright (dont `hanson_wright_noise` et la queue chi-carré `chisq_norm_concentration`), les treize du pont ML (`Bridge`), `#print axioms` sur les théorèmes clés — uniquement les axiomes standards, zéro `sorry` | 40 min | | 21c | [Lean-21c-Descente-Budget](Lean-21c-Descente-Budget.ipynb) | Le budget de descente : quand la décroissance borne le nombre de flips — l'analyse qui fonde le seuil 2·log N de la détection MIMO (#12219) | 35 min |