[Epic Origami] Lean — l'escalier avant l'hommage : replier les echelles externes (Riehl, Axler, lean4game) sur notre serie #24838

Part of #17545

État mesuré au 2026-11-05 (lane myia-po-2023:CoursIA, origin/main lu à l'instant, comptages git ls-tree sur MyIA.AI.Notebooks/SymbolicAI/Lean/, dépôts interrogés par gh api, deux URL vérifiées par curl). Ce bloc ne remplace aucune décision doctrinale : il consigne ce qui est mesuré aujourd'hui et laisse l'historique intact.

Pourquoi cette issue

Le diagnostic du mainteneur, verbatim :

« Notre curriculum Lean est dense, mais la progression pédagogique reste assez discutable. On passe d'une présentation assez sommaire du fonctionnement de base et des tactiques à l'usage en agentique, pas forcément très facile d'accès, puis à des séries d'hommage et des distillation qui nous emmènent assez rapidement dans des sphères stratosphériques des maths pas très accessibles. »

Ce corps est mesuré ci-dessous : il est exact, et il se lit en trois ruptures.

Entre le bloc 1 et le bloc 3, il n'y a aucune marche mathématique : on quitte le mode tactique et l'on arrive directement sur le théorème de sensibilité, Kochen-Specker et le langage grothendieckien. Le bloc 2 n'est pas une marche de mathématiques — c'est un changement d'outil. C'est précisément la rupture décrite.

Ce que cette Epic n'est pas. Elle ne renumérote rien et ne redescend aucun lake : c'est le geste de #17545 (gradation du chemin principal, fille de #5081), qui est vivant et non dormant — mesuré ce jour : GROTH-05-MvPowerSeries livré le 2026-11-01 (#24050), promotion Lean-16a/Lean-16c livrée le 2026-11-04 (#24626). #17545 nomme les marches manquantes et s'interdit explicitement de les écrire. Cette Epic-ci est l'autre moitié : elle apporte les échelles externes nommées à partir desquelles ces marches s'écrivent, et elle les écrit.

Vérifié avant de croire ce corps

Ce que je n'ai pas mesuré, et qui ne doit pas être lu comme acquis : le niveau d'entrée réel de chacun des ~41 carnets du bloc 3 (c'est la lecture que #17545 demande, cellule par cellule) ; la qualité pédagogique effective des dépôts externes au-delà de leur description et de leur licence ; le contenu du cours Mathlib couvert par Lean-06 (je n'ai pas ouvert le carnet).

Ce que la série a déjà, et qu'il ne faut pas diluer

L'échelle ne se construit pas contre l'existant :

• la discipline d'exécution — C.1 (aucune erreur volontaire), C.2 (sorties réelles), et les ratchets de sortie et de source ;
• les lacs formels natifs qui accompagnent les carnets (conway_lean, knot_lean, grothendieck_lean, calibration_lean…) — un carnet de la série n'est pas de la prose sur Lean, c'est du Lean qui compile ;
• l'arc Grothendieck lui-même (« Le charme et la marée », cinq mouvements au README) : il a toute sa place. Il est la destination, pas l'entrée ;
• la discipline d'attribution déjà pratiquée (SocialChoice/Peters, Tao, Sheydvasser, et les issues de distillation) — c'est le modèle à suivre ici, pas à réinventer.

Les échelles externes — mesurées, avec leur licence

La licence décide de ce qu'on a le droit d'en faire. Elle est mesurée, pas supposée.

Trois dépôts sans licence ne sont pas une ressource libre — linear-algebra-done-right-lean, Axler-Solutions et yoneda n'en portent aucune ; un quatrième, VerboseReintroductionToProofs, porte un fichier que GitHub n'identifie pas (NOASSERTION). On les lit pour comprendre une progression et comparer deux façons de traiter le même exercice, et on écrit notre propre code. Aucune ligne n'en est recopiée, aucun fichier n'en est vendu dans le dépôt. Le dire ici évite qu'une lane le découvre après avoir écrit la moitié d'un carnet.

Plis

Pli 1 — L'entrée par le jeu, avant le texte (ouvert maintenant)

Le trou : Lean-01 → Lean-06 explique. Un débutant lit six carnets avant d'avoir rien manipulé. Le mainteneur nomme lean4game « un bijou de gamification à la pédagogie très en avance sur ce qu'on fait dans nos Notebooks ».

• Fille 1.1 — Lean-00 : entrer par le jeu officiel. Installe et lance lean4game localement (lien officiel, jamais vendu), puis cartographie monde du jeu → chapitre de nos carnets : ce que le jeu enseigne en manipulant, ce que Lean-01..06 explicitent ensuite. Critère : la table de correspondance est complète et un débutant peut faire le jeu avant Lean-01.
• Fille 1.2 — la sortie du jeu. Une marche entre le jeu et Lean-06 : passer du monde fermé à un lake personnel qui compile. S'appuie sur ReintroductionToProofs (séminaire de 1ʳᵉ année : c'est exactement le niveau visé) et sur l'idée de verbose-lean4 — une tactique expliquée en langage naturel avant d'être nommée.

Contrainte : ni GPL vendu, ni jeu copié. On écrit un carnet qui conduit au jeu.

Pli 2 — Les catégories : construire l'escalier avant l'hommage (ouvert maintenant)

Le trou, mesuré : l'entrée dans les catégories est un hommage (Lean-15) au 15ᵉ cran, et la visite visuelle (Lean-15d) est le 4ᵉ des 5 carnets du bloc. Yoneda, lui, est enseigné dans Serre100, donc plus loin encore. On demande au lecteur d'admirer un langage avant de lui avoir fait construire une catégorie.

• Fille 2.1 — l'escalier Riehl. Suivre l'ordre du livre (catégorie → foncteur → transformation naturelle → Yoneda → limites → adjonctions) et en faire des marches exécutables, chacune avec un exercice Lean. Comité de lecture : category-theory-in-context-lean (MIT, adaptable) donne la forme Lean ; le livre donne l'ordre, qui est ce qui nous manque.
• Fille 2.2 — où poser cet escalier. Décider et écrire : l'escalier devient-il une base nue dans GROTH/ avant Lean-15, ou une sous-série propre ? La décision appartient à [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545 (elle touche la numérotation) ; cette fille-ci fournit le contenu et l'argument, pas le renommage.
• Fille 2.3 — la marche haute. yoneda (82★) compare 1-catégories et ∞-catégories : c'est la suite naturelle de Serre100/04, pour un lecteur qui a déjà la base. infinity-cosmos reste hors périmètre — c'est une destination de recherche, pas une marche d'entrée.

Ce qui n'est pas demandé : retirer ou réécrire Lean-15. L'hommage reste ; on lui ajoute ce qui manque en dessous.

Pli 3 — Le socle d'algèbre linéaire (ouvert maintenant)

Le trou, mesuré et le plus net de tous : aucun carnet d'algèbre linéaire dans la série, aucune mention au README. On saute du tutoriel de langage à Lean-12 (sensibilité), Lean-13 (Kochen-Specker, CHSH : espaces de Hilbert de dimension finie, produits scalaires) et Lean-15 (catégories), qui tous en dépendent.

• Fille 3.1 — la marche Axler. Une progression d'algèbre linéaire en Lean avant Lean-12 : espaces vectoriels, applications linéaires, valeurs propres, produit scalaire, opérateurs. Axler est en accès libre (200 OK) et son ordre est délibérément non-standard (déterminants en dernier) — c'est un choix pédagogique à examiner, pas à recopier.
• Fille 3.2 — la comparaison des deux compagnons. linear-algebra-done-right-lean (Lean, sans licence) et Axler-Solutions (LaTeX, sans licence) traitent le même livre de deux façons. Les comparer pour choisir la meilleure distillation — quel exercice se prête au formel, lequel se prête à la solution écrite. Lecture seule, aucune recopie.

Pli 4 — La combinatoire, là où notre dépôt résonne déjà (ouvert quand le pli 3 a rendu sa mesure)

Le mainteneur note enumerative-chromatic-choosability « en résonance avec notre dépôt ». Mesuré : la résonance est réelle et double.

• Lean-27-EdgeColoring-Tutte (coloration d'arêtes, conjecture de Tutte) — 10 cellules, compagnon formel d'un carnet Python de Search/Part5-Frontieres : c'est une marche fine, pas un socle.

• ANALYSE-08-Ramsey-VdW — 29 cellules, deux théorèmes exacts prouvés par épuisement, puis le mur où l'énumération s'arrête.

• Fille 4.1 — coloriage de listes. Distiller enumerative-chromatic-choosability (Apache-2.0, adaptable avec attribution ; source Kirov & Naimi, Ars Combin. 124) : la fonction de coloriage de listes comme troisième marche après la coloration d'arêtes de Lean-27 et avant l'énumération de ANALYSE-08. L'apport propre du dépôt amont est un compagnon en Verso — une forme de documentation que nous n'utilisons pas.

Pourquoi ce pli attend : il suppose une base de combinatoire et de graphes que le pli 3 rend explicite. L'ouvrir avant serait ajouter une marche sans son socle — exactement le défaut que cette Epic corrige.

Pli 5 — Arbitrages

• Licences. Deux dépôts sans licence sont en lecture seule (plis 3). Si une lane veut en dériver du code, c'est une question à poser à l'auteur, pas une décision de lane.
• Ce qu'on ne fait pas : ni copier, ni vendorer les ressources Lean de la planète — le mainteneur l'a dit et la mesure le confirme : il y a de quoi remplir dix séries, ce n'est pas le but. Chaque pli cite peu de sources et les cite bien.
• Dépôts biblio : Riehl et Axler avant d'écrire les carnets correspondants, pas après (bibliography-hygiene : la copie archivée est ce contre quoi on relit ce qu'on a écrit).
• Numérotation : aucune décision de cette Epic ne renomme un carnet. Les filles 2.2 fournissent l'argument ; le geste est celui de [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545 / [EPIC] Nommage canonique et parcours des notebooks — numéros, accrétions, noyaux et catalogue #5081.
• Veto carnets Physique — Relativité numérique : grain ouvert (T3 de #23161) #24439 : cette Epic produit des carnets neufs, elle y est donc soumise. Rien ici ne contourne le veto — les filles se claimeront quand le pool le permet, ou les marches s'écriront en fichiers .lean quand c'est possible.

Tableau des thèmes et de leur état

Critères de sortie

1. Une marche existe entre Lean-06 et Lean-12 qui ne suppose que Lean-01..06 — prouvée par ses prérequis écrits, pas par son titre.
2. Le bloc catégories a une entrée de niveau licence avant Lean-15, et cette entrée est EXEC_PROVED (C.2, sorties réelles) — pas un panorama.
3. Lean-12 et Lean-13 ne sont plus les premiers carnets à supposer l'algèbre linéaire.
4. Chaque carnet neuf cite sa source et sa licence, et aucun ne contient de code recopié d'un dépôt sans licence.
5. Riehl et Axler sont archivés avec leur chemin GDrive cité dans la PR correspondante.
6. Aucun carnet existant n'est retiré : cette Epic ajoute des marches, elle ne déplace pas les destinations (geste [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545).

Non-buts

• Pas de renumérotation, pas de redescente de lake : [Lean] Gradation du chemin principal a partir de Lean-10 + sous-series (Lean et IA, Conway, verification, formalisations) — fille #5081 #17545 et [EPIC] Nommage canonique et parcours des notebooks — numéros, accrétions, noyaux et catalogue #5081.
• Pas de réécriture de l'arc Grothendieck : il est la destination.
• Pas de vendoring, pas de copie de dépôt tiers.
• Pas de nouveau lake par pli : un lake ne s'ajoute que si une marche en a besoin pour compiler.