Lean-20 : Capstone — digérer le travail formel de Tao (sous-série ANALYSE)

Série : SymbolicAI / Lean — escalier vers la sous-série ANALYSE

Navigation

Notebook précédent	Notebook suivant
Lean-17c - Knots Companion Formel	ANALYSE-01 - Sendov pour entrer dans la sous-série, ou Lean-21 - MIMO Detection Flips pour poursuivre le parcours principal

Ce capstone est l’escalier de la série Lean vers sa sous-série ANALYSE, 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.

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.

Prérequis : le tutoriel de la série (numéros 1 à 6). Durée : 25 min. Kernel : python3, bibliothèque standard seule.

1. Le geste : digérer, pas seulement vérifier

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) rappelle la hiérarchie : « Solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight. »

Une preuve vérifiée par Lean n’est pas encore une preuve comprise. La sous-série pratique la digestion à travers quatre gestes :

Geste	Ce qu’il produit	Où
Lire le lac	l’architecture de la preuve, fichier par fichier	ANALYSE-01, ANALYSE-02, ANALYSE-03
Raconter	l’énoncé, ses cas, son contexte, dans une langue lisible	ANALYSE-01, ANALYSE-03
Extraire	les primitives réutilisables hors du cadre d’origine	ANALYSE-04
Admettre	l’endroit exact où une primitive cesse de valoir	ANALYSE-04

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.

2. Où entrer : les quatre carnets

La sous-série vit dans le dossier ANALYSE/ : quatre carnets et un README.

#	Carnet	Ce qu’il digère	Lac source
01	Sendov	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`
02	Analysis I	le manuel de Tao en Lean 4 : architecture du lac, auto-contenance face à Mathlib, cinq lemmes emblématiques	`teorth/analysis`
03	PFR	la conjecture de Freiman-Ruzsa polynomiale sur F₂ⁿ et sa méthode entropique, avec des `#check` réels sur le lac compilé	`teorth/pfr`
04	Primitives de PFR	trois primitives de la preuve, et l’endroit exact où chacune cesse de valoir	`teorth/pfr`

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.

3. Le versant formel : trois lacs externes

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 :

PFR_conjecture, la version combinatoire ;
entropic_PFR_conjecture, la version entropique, formalisée en premier ;
rdist, la distance entropique de Ruzsa ;
tau_strictly_decreases, la descente stricte de la fonctionnelle τ qui fait avancer la preuve.

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.

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

\[d[X_1 ; U_H] + d[X_2 ; U_H] \le 11 \cdot d[X_1 ; X_2],\]

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 ».

4. La marche : deux primitives de PFR à la main

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).

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.
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.

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.

# Deux primitives de PFR, calculees a la main sur le groupe F_2^3.
# Copie pedagogique declaree : la digestion complete vit dans ANALYSE-04.
from itertools import combinations
from math import log2

ELEMENTS = range(8)  # F_2^3, un element = un entier de 3 bits, addition = XOR


def entropie(loi):
    """Entropie de Shannon (en bits) d'une loi {valeur: probabilite}."""
    return -sum(p * log2(p) for p in loi.values() if p > 0)


def loi_image(loi, f):
    """Loi de f(X) quand X suit `loi`."""
    image = {}
    for x, p in loi.items():
        image[f(x)] = image.get(f(x), 0.0) + p
    return image


def entropie_conditionnelle(loi, f):
    """H(X | f(X)) : moyenne des entropies de X sur chaque fibre de f."""
    total = 0.0
    for c, pc in loi_image(loi, f).items():
        fibre = {x: p / pc for x, p in loi.items() if f(x) == c}
        total += pc * entropie(fibre)
    return total


def somme_independante(loi_x, loi_y):
    """Loi de X' - Y' pour des copies independantes (dans F_2^3, - = XOR)."""
    somme = {}
    for x, p in loi_x.items():
        for y, q in loi_y.items():
            somme[x ^ y] = somme.get(x ^ y, 0.0) + p * q
    return somme


def distance_ruzsa(loi_x, loi_y):
    """Distance entropique de Ruzsa d[X ; Y] = H(X' - Y') - H(X)/2 - H(Y)/2."""
    return entropie(somme_independante(loi_x, loi_y)) - entropie(loi_x) / 2 - entropie(loi_y) / 2


def sous_groupes():
    """Les 16 sous-espaces de F_2^3, engendres par toutes les familles de vecteurs."""
    vus = set()
    for k in range(4):
        for famille in combinations(range(1, 8), k):
            engendre = {0}
            for v in famille:
                engendre |= {x ^ v for x in engendre}
            vus.add(frozenset(engendre))
    return sorted(vus, key=lambda h: (len(h), sorted(h)))


def uniforme(ensemble):
    return {x: 1 / len(ensemble) for x in ensemble}


# Primitive 2 : projection / fibres. Quotient par le sous-groupe H = {000, 001}.
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}
classe = lambda x: x & 0b110  # representant de la classe x + H
h_x = entropie(X)
h_pi = entropie(loi_image(X, classe))
h_fibres = entropie_conditionnelle(X, classe)
print("Primitive 2 -- regle de chaine H(X) = H(pi(X)) + H(X | pi(X))")
print("  H(X)          = %.6f bits" % h_x)
print("  H(pi(X))      = %.6f bits  (4 classes)" % h_pi)
print("  H(X | pi(X))  = %.6f bits  (moyenne sur les fibres)" % h_fibres)
print("  ecart         = %.2e" % abs(h_x - (h_pi + h_fibres)))

# Primitive 1 : distance de Ruzsa, et le signal compression => structure.
groupes = sous_groupes()
print("\nPrimitive 1 -- distance de Ruzsa sur %d sous-groupes de F_2^3" % len(groupes))
print("  %-28s %10s %14s %8s" % ("loi de X", "d[X;X]", "min_H d[X;U_H]", "|H*|"))
U_sg = uniforme({0, 1, 2, 3})
for eps in (0.0, 0.1, 0.3, 0.6, 1.0):
    loi = {x: (1 - eps) * U_sg.get(x, 0.0) + eps / 8 for x in ELEMENTS}
    d_xx = distance_ruzsa(loi, loi)
    meilleur = min(groupes, key=lambda h: distance_ruzsa(loi, uniforme(h)))
    d_xh = distance_ruzsa(loi, uniforme(meilleur))
    print("  %-28s %10.4f %14.4f %8d" % ("melange eps=%.1f" % eps, d_xx, d_xh, len(meilleur)))
d_xx = distance_ruzsa(X, X)
meilleur = min(groupes, key=lambda h: distance_ruzsa(X, uniforme(h)))
print("  %-28s %10.4f %14.4f %8d" % ("X de la primitive 2", d_xx, distance_ruzsa(X, uniforme(meilleur)), len(meilleur)))

Primitive 2 -- regle de chaine H(X) = H(pi(X)) + H(X | pi(X))
  H(X)          = 2.708695 bits
  H(pi(X))      = 1.760964 bits  (4 classes)
  H(X | pi(X))  = 0.947731 bits  (moyenne sur les fibres)
  ecart         = 0.00e+00

Primitive 1 -- distance de Ruzsa sur 16 sous-groupes de F_2^3
  loi de X                         d[X;X] min_H d[X;U_H]     |H*|
  melange eps=0.0                  0.0000         0.0000        4
  melange eps=0.1                  0.1665         0.1432        4
  melange eps=0.3                  0.2093         0.1951        8
  melange eps=0.6                  0.1002         0.0594        8
  melange eps=1.0                  0.0000         0.0000        8
  X de la primitive 2              0.2520         0.1457        8

Lecture du résultat

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.
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.
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.

5. Mesurer la surface de la sous-série

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 :

le noyau déclaré ;
le nombre de cellules de code et combien portent une trace d’exécution ;
le nombre de titres d’exercice ;
le nombre de déclarations distinctes passées à #check ;
les lacs teorth cités ;
le premier titre.

Elle rend aussi visible ce que la description ne dit pas.

# Surface de la sous-serie : on lit les carnets, on ne suppose rien.
import json
import os
import re

RACINE = "ANALYSE"


def fiche(chemin):
    """Kernel, cellules executees, exercices, lacs cites et titre d'un carnet."""
    with open(chemin, encoding="utf-8") as f:
        carnet = json.load(f)
    cellules = carnet["cells"]
    code = [c for c in cellules if c["cell_type"] == "code"]
    texte = "\n".join("".join(c["source"]) for c in cellules)
    titre = next(
        (ligne for c in cellules if c["cell_type"] == "markdown"
         for ligne in "".join(c["source"]).splitlines() if ligne.startswith("# ")),
        "(aucun titre)",
    )
    return {
        "kernel": carnet["metadata"].get("kernelspec", {}).get("name", "?"),
        "code": len(code),
        "executees": sum(1 for c in code if c.get("execution_count") is not None),
        "exercices": len(re.findall(r"(?m)^#{3,4} *(?:[\d.]+ *)?Exercice\b", texte)),
        "lacs": sorted(set(re.findall(r"teorth/[\w-]+", texte))),
        "checks": len(set(re.findall(r"#check\s+@?([\w.]+)", texte))),
        "titre": titre[2:62],
    }


carnets = sorted(n for n in os.listdir(RACINE) if n.endswith(".ipynb"))
print("%-40s %-10s %6s %6s %5s %6s" % ("carnet", "kernel", "code", "exec", "exos", "#check"))
fiches = {}
for nom in carnets:
    f = fiches[nom] = fiche(os.path.join(RACINE, nom))
    print("%-40s %-10s %6d %6d %5d %6d" % (nom[:40], f["kernel"], f["code"], f["executees"], f["exercices"], f["checks"]))

print("\nLacs externes cites :", sorted({l for f in fiches.values() for l in f["lacs"]}))
print("\nPremier titre de chaque carnet :")
for nom, f in fiches.items():
    print("  %-12s -> %s" % (nom[:11], f["titre"]))

carnet                                   kernel       code   exec  exos #check
ANALYSE-01-Sendov-Lean-Python.ipynb      python3        10     10     3      1
ANALYSE-02-Tao-Lean-Python.ipynb         python3         9      9     3      1
ANALYSE-03-PFR-Lean.ipynb                lean4-wsl       9      9     3     17
ANALYSE-04-PFR-Primitives-Python.ipynb   python3         6      6     0      0

Lacs externes cites : ['teorth/analysis', 'teorth/pfr', 'teorth/sendov']

Premier titre de chaque carnet :
  ANALYSE-01-  -> Lean-18 : La Conjecture de Sendov (preuve L. Mazur, digestio
  ANALYSE-02-  -> Lean-19 : Le manuel *Analysis I* de T. Tao en Lean 4 (lac `t
  ANALYSE-03-  -> Lean-20 : La conjecture de Freiman-Ruzsa polynomiale (PFR) —
  ANALYSE-04-  -> Lean-20b : Trois primitives de PFR, et l'endroit exact où el

Lecture du résultat

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.
Toutes les cellules de code portent une trace d’exécution (10/10, 9/9, 9/9, 6/6).
Trois exercices dans chacun des trois premiers carnets, aucun dans ANALYSE-04. C’est un écart à la convention des trois exercices par carnet.
Trois lacs externes, tous publiés par Tao : teorth/sendov, teorth/analysis, teorth/pfr.
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.

Les deux derniers défauts, avec le nom du dossier, sont suivis dans l’issue #18408. Cette mesure s’appuie sur les carnets eux-mêmes : elle suivra leur correction sans qu’on ait à réécrire cette section.

6. Exercices

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.

Exercice 1 — la règle de chaîne pour un autre quotient

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.

É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.

Indice : la classe de x modulo H₂ est {x, x ^ 0b110}. Son plus petit élément en est un représentant.

# Exercice 1 : la regle de chaine pour le quotient par H2 = {000, 110}.


def classe_h2(x):
    """Representant de la classe de x modulo H2 = {000, 110}."""
    # TODO etudiant : rendre le plus petit des deux elements x et x ^ 0b110.
    return None


if classe_h2(0) is None:
    print("Exercice 1 a completer : definir classe_h2, puis verifier la regle de chaine.")
else:
    ecart = entropie(X) - entropie(loi_image(X, classe_h2)) - entropie_conditionnelle(X, classe_h2)
    print("Ecart de la regle de chaine pour H2 : %.2e" % abs(ecart))

Exercice 1 a completer : definir classe_h2, puis verifier la regle de chaine.

Exercice 2 — une classe latérale est aussi structurée qu’un sous-groupe

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.

É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}.

Indice : dans F₂³, X + v s’écrit x ^ v élément par élément. La probabilité ne change pas, seule l’étiquette bouge.

# Exercice 2 : invariance de la distance de Ruzsa par translation.


def loi_translatee(loi, v):
    """Loi de X + v quand X suit `loi` (dans F_2^3, + = XOR)."""
    # TODO etudiant : rendre le dictionnaire {x ^ v: p}.
    return None


if loi_translatee(X, 1) is None:
    print("Exercice 2 a completer : definir loi_translatee, puis comparer les distances.")
else:
    for v in ELEMENTS:
        Xv = loi_translatee(X, v)
        print("v = %d : d[X+v ; X+v] = %.6f" % (v, distance_ruzsa(Xv, Xv)))
    classe_laterale = uniforme({4, 5, 6, 7})
    print("d[U ; U] sur la classe laterale :", distance_ruzsa(classe_laterale, classe_laterale))

Exercice 2 a completer : definir loi_translatee, puis comparer les distances.

Exercice 3 — les titres attendus, calculés depuis les noms de fichier

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.

É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.

Indice : re.match(r"(ANALYSE-\d+)", nom) isole l’identifiant, et fiches[nom]["titre"] donne le titre sans son #.

# Exercice 3 : les carnets dont le titre ne porte pas l'identifiant du fichier.


def titres_en_ecart(fiches):
    """Liste des couples (carnet, titre actuel) dont le titre ne commence pas par l'identifiant."""
    # TODO etudiant : deduire l'identifiant du nom de fichier, le comparer au
    # debut du titre, et rendre les couples en ecart.
    return None


resultat = titres_en_ecart(fiches)
print("Exercice 3 a completer" if resultat is None else resultat)

Exercice 3 a completer

7. Conclusion — ce que ce capstone laisse au lecteur

Un point d’entrée. La sous-série ANALYSE 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).
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.
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.
Une surface mesurée, avec ses défauts. Les titres, les exercices d’ANALYSE-04 et le nom du dossier sont suivis dans #18408.

Suite. Entrer par ANALYSE-01, ou poursuivre le parcours principal avec Lean-21. 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).

Retour au sommet