Ce capstone est l’escalier de la série Lean vers sa sous-série Serre 100 : il la présente — par où y entrer, ce qu’elle démontre, ce qu’elle suppose — et cite son lake compagnonserre100_lean/. Le lecteur du parcours principal voit ainsi le résultat formel sans avoir à entrer dans la sous-série.
La sous-série est née du centenaire de Jean-Pierre Serre (conférence Serre 100, 15-16 septembre 2026) — EPIC #16334.
Kernel : Python 3 (bibliothèque standard seule). Le versant preuves de la sous-série vit dans le lake et s’exécute avec le kernel lean4-wsl (installation : Lean-01-Setup-Lean-Python).
Durée estimée : 20 minutes (présentation + une mesure de la surface de la sous-série).
1. Le geste : distiller un énoncé en un calcul
Une distillation prend un énoncé ou une construction centrale de Serre et le rend calculé dans une sortie : l’énoncé devient une expérience numérique vérifiable, démontrable en Lean quand Mathlib le permet, et exerçable.
Chaque carnet de la sous-série a donc deux versants, et c’est ce diptyque qui la structure :
Versant
Où il vit
Ce qu’il fait
La mesure
le carnet (kernel python3)
l’énoncé devient un tableau, une figure, une identité vérifiée sur des données
le même énoncé est démontré, ou vérifié par le noyau sur les mêmes instances
Le carnet mesure, le lake prouve. Lire l’un sans l’autre laisse la moitié du geste de côté — c’est pourquoi ce capstone cite le lake nommément, section 3.
2. Où entrer : les huit carnets
La sous-série vit dans le dossier Serre100/ — huit carnets, un README et le lake. Le tableau dit, par carnet, ce qu’il distille.
le tour des cinq monuments de Serre présents dans Mathlib
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.
3. Le versant preuves : le lake serre100_lean
Le lake Serre100/serre100_lean/ porte cinq modules et leurs miroirs i18n _en (convention sibling pair de l’EPIC #4980), pinnés sur les mêmes références Mathlib que hecke_lean. Chacun adosse un carnet de la sous-série à de vraies déclarations — c’est la citation qui donne au parcours principal son résultat formel :
hX_app, evaluation_eq, round_trip_domain, round_trip_codomain, natEquiv_apply, card_nat_eq_homCard, fidelite — et pont_cech pour le pont Serre-Grothendieck
Deux carnets n’ont pas encore de module : 06 (bulles de Minkowski) et 07 (gaps et statistique GUE) sont, à ce jour, du versant mesure seul.
Les deux racines agrégateurs Serre100.lean et Serre100_en.lean importent Tour, HasseComputee et CaracteresComputes. MZVFinies et YonedaCalcule sont tout de même buildés — le lakefile globbe les sous-modules Serre100 (FR et _en) — mais un import Serre100 ne les met pas en portée.
Pour exécuter le versant preuves, la procédure (kernel lean4-wsl, lake build, prérequis de l’environnement partagé) est celle du carnet 08.
4. Ce que la sous-série suppose
Rien à installer pour les carnets de mesure : ils tournent sur le kernel python3, et la sous-série déclare dans son README une « arithmétique en stdlib pur (aucune dépendance au-delà de matplotlib pour les figures) ». Le carnet de preuves (08) suppose, lui, le kernel lean4-wsl et un lake déjà construit.
Cette phrase est une affirmation de la sous-série à propos d’elle-même — exactement le genre d’affirmation qu’on vérifie plutôt qu’on ne la croit. La section suivante la mesure.
5. Mesurer la surface de la sous-série
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.
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.
# Dependances de la sous-serie : on lit les carnets, on ne suppose rien.import astimport ioimport jsonimport osimport sysRACINE ="Serre100"STDLIB =set(sys.stdlib_module_names)def importations(notebook):"""Importations de premier niveau des cellules de code d'un notebook. Rend aussi le nombre de cellules de code que `ast` ne sait pas lire (magics, ou code Lean du carnet 08) : sans ce compteur, un carnet entier pourrait passer pour un carnet sans dependance. """ trouves =set() illisibles =0for cell in notebook["cells"]:if cell.get("cell_type") !="code":continue source ="".join(cell.get("source", []))try: arbre = ast.parse(source)exceptSyntaxError: illisibles +=1continuefor noeud in ast.walk(arbre):ifisinstance(noeud, ast.Import):for alias in noeud.names: trouves.add(alias.name.split(".")[0])elifisinstance(noeud, ast.ImportFrom) and noeud.level ==0and noeud.module: trouves.add(noeud.module.split(".")[0])return trouves, illisiblescarnets =sorted(f for f in os.listdir(RACINE) if f.endswith(".ipynb"))print("%d carnets dans %s/"% (len(carnets), RACINE))print()print("%-42s%-10s%-14s%s"% ("carnet", "kernel", "cells hors AST", "imports hors stdlib"))print("-"*94)dependances =set()for nom in carnets: notebook = json.load(io.open(os.path.join(RACINE, nom), encoding="utf-8")) kernel = notebook.get("metadata", {}).get("kernelspec", {}).get("name", "?") trouves, illisibles = importations(notebook) externes =sorted(m for m in trouves if m notin STDLIB andnot m.startswith("_")) dependances.update(externes)print("%-42s%-10s%-14s%s"% ( nom, kernel, str(illisibles) if illisibles else"-",", ".join(externes) if externes else"aucun"))print()print("Dependances externes de toute la sous-serie : %s"%", ".join(sorted(dependances)))
La mesure confirme le diptyque et précise la convention déclarée :
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.
La sous-série est bien portée par la bibliothèque standard : aucune dépendance de calcul n’apparaît.
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.
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.
6. Exercices
Les trois exercices prolongent 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 — où numpy est-il employé, et pour quoi ?
L’audit dit que05 et 06 importent numpy. Il ne dit pas à quoi il sert, et la différence compte : une dépendance de figure n’engage pas la même chose qu’une dépendance de calcul. Écrire la fonction qui relève les usages np.* cellule par cellule.
Étapes : (1) parcourir les cellules de code du carnet ; (2) retenir celles qui emploient np. et compter les usages ; (3) rendre la liste des couples (indice de cellule, nombre d'usages).
Indice : l’expression régulière r"\bnp\.[A-Za-z_]\w*" et re.findall donnent directement la liste des usages d’une cellule.
# Exercice 1 : les usages de numpy, cellule par cellule.import redef usages_numpy(nom_carnet):"""Liste des couples (indice de cellule, nombre d'usages np.*). Les cellules sans usage numpy ne sont pas rendues. """# TODO etudiant : lire le notebook, parcourir ses cellules de code,# compter les usages de `np.` et retourner les couples non nuls.returnNonefor carnet in ("05-table-de-caracteres.ipynb", "06-bulles-minkowski.ipynb"): resultat = usages_numpy(carnet)print("Exercice 1 a completer — %s : %s"% (carnet, resultat))
Exercice 1 a completer — 05-table-de-caracteres.ipynb : None
Exercice 1 a completer — 06-bulles-minkowski.ipynb : None
Exercice 2 — élargir le périmètre de l’audit
L’audit porte sur Serre100/. La question « de quoi la série Lean a-t-elle besoin ? » se pose à l’échelle de toute la série : une soixantaine de carnets à la racine, plus la sous-série. Écrire le recensement par kernel, récursif, et l’appliquer à la racine.
Étapes : (1) parcourir récursivement le dossier (les carnets de la sous-série sont un niveau plus bas) ; (2) lire le kernel déclaré par chacun ; (3) rendre un dictionnaire {kernel: nombre de carnets}.
Indice : os.walk plus la clé metadata.kernelspec.name suffisent. Attendu : les carnets Lean natifs et les carnets Python se séparent nettement.
# Exercice 2 : recensement des kernels sur toute la serie Lean.import osdef recensement_kernels(racine):"""Dictionnaire {nom de kernel: nombre de carnets} sous `racine`, recursif."""# TODO etudiant : parcourir recursivement, lire le kernelspec de chaque# carnet et agreger les comptes par kernel.returnNoneprint("Exercice 2 a completer — recensement :", recensement_kernels("."))
Exercice 2 a completer — recensement : None
Exercice 3 — la table des matières qui ne périme pas
La table de la section 2 a été écrite à la main ; c’est exactement ce qui la laisse dériver quand un carnet change de titre ou quand un neuvième carnet arrive — la sous-série en a déjà fait l’expérience. Écrire la fonction qui régénère cette table depuis les premiers titres des carnets.
Étapes : (1) parcourir les carnets du dossier dans l’ordre alphabétique ; (2) extraire le premier titre markdown de niveau 1 ; (3) rendre une ligne de tableau markdown par carnet.
Indice : dans le JSON d’un notebook, un titre de niveau 1 est une cellule markdown dont la source commence par #. La bibliothèque re et json suffisent.
# Exercice 3 : regenerer la table des matieres depuis les carnets.import jsondef table_depuis_titres(dossier):"""Lignes markdown `| carnet | titre |` extraites des titres de niveau 1."""# TODO etudiant : pour chaque carnet du dossier, extraire le premier# titre de niveau 1 et construire la ligne de tableau correspondante.returnNonelignes = table_depuis_titres(RACINE)print("Exercice 3 a completer — table :", lignes)
Exercice 3 a completer — table : None
7. Conclusion — ce que ce capstone laisse au lecteur
Trois choses, dans cet ordre :
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/ est son README.
Un résultat formel cité : le lake 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 les fait tourner dans un noyau Lean réel.
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.
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.