État mesuré au 2026-10-05 (consolidation #13906, lane myia-po-2025:CoursIA). Confrontation des 8 workstreams et des 6 critères d'acceptation à origin/main. L'Epic n'est pas fermable : 12 cases sur 14 sont tenues, 2 ne le sont pas — elles sont nommées ci-dessous, avec leur artefact.
Workstreams
| # |
Workstream |
Verdict |
Artefact vérifié sur main |
| 1 |
Comparer Sendov, Analysis I et PFR comme baselines |
tenue |
ANALYSE-01 (Sendov), ANALYSE-02 (Tao, Analysis I), ANALYSE-03 (PFR), ANALYSE-04 (primitives) + capstone Lean-20 §3-§5 : les trois lacs teorth sont cités par #check réel et la surface de la sous-série est mesurée par lecture des quatre carnets |
| 2 |
Appliquer la grille aux résultats Palomar, verdict par résultat, AUCUNE ACTION compris |
tenue |
#13107 (ouverte) — inventaire 68/68 résultat par résultat, verdicts fermés, VEILLE et AUCUNE ACTION présents et assumés comme conclusions normales |
| 3 |
Pilote quantique CHSH / Tsirelson / Landau |
tenue |
Conway/CHSH.lean, CHSHRandomized.lean, CHSHQuantum.lean, CHSHLandau.lean, CHSHFreeWill.lean sur main ; PRs #14132, #14858, #16177, #17279, #19020 toutes MERGED |
| 4 |
Pilote de traçabilité (snapshot, provenance, réserves de registre) |
tenue |
ANALYSE-03, section « Provenance, priorité et nouveauté réelle » — le certificat formel est muet sur qui, ce qu'il ajoute et jusqu'où il porte ; #13107 §« Snapshot et méthode » |
| 5 |
Pilote narratif Erdős / formal-conjectures → Lean-7b / Lean-8 |
tenue |
Lean-08b-Erdos-Formal-Conjectures-Lean.ipynb sur main ; #15209 et #16545 MERGED ; volet PFR porté par #15842 et #15869 |
| 6 |
Pilote calculatoire borné (topologies finies, mélange, low-rank SOS) |
tenue |
Search-09b-SpuriousMinima.ipynb sur main ; #13197 MERGED (recensement Burer-Monteiro) |
| 7 |
Veille des proximités sans ancrage CoursIA |
tenue |
#13107 range les quatre familles nommées avec un verdict : Scott 1982, jacobienne (entrées 14, 17, 31), produits séquentiels (26, 34, 43), algèbre de Jordan explicitement écartée |
| 8 |
Relier la digestion à la revue éditoriale |
tenue |
docs/cadrage/leiden-declaration-position.md (30 696 o) fixe la doctrine. Le body ci-dessous cite docs/leiden-declaration-position.md, chemin qui n'existe pas — le fichier vit sous docs/cadrage/. Référence corrigée dans ce bloc. |
Critères d'acceptation
| # |
Critère |
Verdict |
Preuve / ce qui manque |
| 1 |
Au moins trois pilotes de familles différentes satisfont la grille |
tenue |
trois familles distinctes : quantique (WS3), narratif Erdős (WS5), calculatoire borné (WS6) |
| 2 |
Chaque pilote porte une revue humaine nommée |
NON TENUE |
MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean/README.md:403 le déclare lui-même : « aucune revue humaine nommée du lake entier n'a eu lieu. C'est une limite déclarée de la présente digestion (grille #13106 point 10) ». La revue humaine existe comme exigence et comme questions (Lean-07b, « Questions pour la revue humaine »), pas comme acte nommé par pilote. |
| 3 |
Au moins un pilote conserve un chemin de découverte ou un échec instructif |
tenue |
#15842 §8 « Friction et chemin de découverte » ; #15869 items 6/7 Lean-21b |
| 4 |
Au moins un pilote compare le certificat formel à l'exposition informelle |
tenue |
ANALYSE-03 : « Un certificat formel atteste qu'une preuve est close. Il ne dit ni de qui elle vient, ni ce qu'elle ajoute, ni jusqu'où elle porte. » |
| 5 |
Les lacunes bibliographiques ou d'attribution sont traitées ou conservées explicitement |
tenue |
ANALYSE-03 « Qui a conjecturé, qui a publié, qui est crédité » (attribution Marton/Ruzsa) ; #13107 conserve les warnings de review et les AUCUNE ACTION |
| 6 |
Une synthèse transverse relie les pilotes sans proclamer la canonicalisation achevée |
NON TENUE |
Aucune synthèse transverse n'existe. Les documents qui citent ≥2 carnets-pilotes sont soit générés (docs/curriculum/ia-symbolique.md, docs/curriculum/recherche.md — generate_parcours.py, écrasés au prochain cron), soit hors sujet (docs/ict/dissociations-matrix.md : le CHSH y est le toy de Spekkens, série ICT). Un tableau de catalogue n'est pas une synthèse. |
Ce qui reste, et où ça vit
- Revue humaine nommée sur les pilotes qui satisfont la grille (critère 2) — le dépôt nomme lui-même ce manque ; c'est un acte de relecture à inscrire dans le README du lake concerné.
- Synthèse transverse des pilotes (critère 6), distincte du catalogue généré : elle doit relier les pilotes entre eux sans conclure la canonicalisation sur un build vert.
Les deux résidus sont actionnables par une lane ; aucun n'est verrouillé par une décision user.
Portée non vérifiée : les revues humaines ont été cherchées dans docs/, les notebooks Lean et les README de lake, pas dans les fils d'issue des 21 PRs qui citent cet Epic — une relecture consignée en commentaire de PR ne serait pas vue ici.
Pourquoi cet Epic
Terry Tao distingue, dans Mathematics in the Age of AI (ICM 2026), cinq opérations que l’accélération technique tend à confondre : générer une preuve, la vérifier, l’exposer, la publier, puis la digérer et la canonicaliser. La dernière étape — intégrer le résultat à un corpus cohérent, attribué, compréhensible et enseignable — est la plus lente et la moins automatisable.
CoursIA possède déjà trois cas utiles : Lean-19 Sendov, Lean-20 Analysis I et Lean-21 PFR. L’Epic fermé #10763 portait deux livrables précis ; le présent Epic ne le rouvre pas. Il généralise la méthode à tout résultat formel, computationnel ou fortement assisté par IA dont la certification peut dépasser l’exposition humaine.
Le premier banc d’essai exhaustif sera le registre Palomar : ses entrées certifient des snapshots Lean sélectionnés, mais ni la nouveauté, ni l’importance, ni la lisibilité, ni la maturité d’un lake entier. Une présence dans Palomar ne déclenche donc jamais un import automatique.
Risque traité : l’indigestion de preuve
- trivialités surdéveloppées et portion réellement nouvelle sous-exposée ;
- prose « slick » qui efface la friction naturelle et la carte des difficultés ;
- certificat valide présenté sans provenance, littérature, priorité ou attribution suffisantes ;
- chemin de découverte, essais ratés et choix intermédiaires supprimés ;
- build vert confondu avec compréhension, exposition ou canonicalisation ;
- génération plus rapide que la capacité humaine de revue, de publication et d’absorption.
Grille obligatoire d’une digestion
Chaque grain enfant documente :
- l’énoncé exact et le niveau de garantie ;
- la provenance, la littérature, la priorité et l’attribution ;
- la nouveauté réelle par rapport aux dépendances ;
- la carte des dépendances, toolchain, axiomes et hypothèses nommées ;
- les portions triviales condensées et les portions nouvelles ou difficiles développées ;
- la friction naturelle : obstacles, pivots, choix, essais ratés utiles et dette résiduelle ;
- le chemin de découverte, distingué de la reconstruction finale ;
- les limites, claims non établis et réserves de review ;
- le raccord au corpus CoursIA et les prérequis ;
- la transmission : exemple calculé, visualisation ou exercice, plus une revue humaine nommée.
Un inventaire de théorèmes, un certificat seul ou une prose fluide sans carte de difficulté ne satisfont pas cette grille.
Workstreams
Critères d’acceptation
Références
État vérifié — registre Palomar, 2026-08-30
La réfutation Vibe interprète « le premier banc d’essai exhaustif sera le registre Palomar » comme l’affirmation que Palomar était déjà intégré au dépôt au moment de l’ouverture. Ce n’est pas ce que dit le body : le futur décrit un workstream planifié, non un état courant. L’absence locale alors observée ne réfute donc pas cette phrase.
L’état courant matérialise désormais ce workstream sans transformer Palomar en backlog :
Verdict : RÉFUTATION REJETÉE. La formulation initiale était prospective et exacte ; elle possède aujourd’hui un inventaire et une doctrine vérifiables, mais l’Epic reste ouvert.
Pourquoi cet Epic
Terry Tao distingue, dans Mathematics in the Age of AI (ICM 2026), cinq opérations que l’accélération technique tend à confondre : générer une preuve, la vérifier, l’exposer, la publier, puis la digérer et la canonicaliser. La dernière étape — intégrer le résultat à un corpus cohérent, attribué, compréhensible et enseignable — est la plus lente et la moins automatisable.
CoursIA possède déjà trois cas utiles : Lean-19 Sendov, Lean-20 Analysis I et Lean-21 PFR. L’Epic fermé #10763 portait deux livrables précis ; le présent Epic ne le rouvre pas. Il généralise la méthode à tout résultat formel, computationnel ou fortement assisté par IA dont la certification peut dépasser l’exposition humaine.
Le premier banc d’essai exhaustif sera le registre Palomar : ses entrées certifient des snapshots Lean sélectionnés, mais ni la nouveauté, ni l’importance, ni la lisibilité, ni la maturité d’un lake entier. Une présence dans Palomar ne déclenche donc jamais un import automatique.
Risque traité : l’indigestion de preuve
Grille obligatoire d’une digestion
Chaque grain enfant documente :
Un inventaire de théorèmes, un certificat seul ou une prose fluide sans carte de difficulté ne satisfont pas cette grille.
Workstreams
AUCUNE ACTION.Critères d’acceptation
Références
docs/grothendieckian-lens.mdetdocs/magnifica-humanitas-dialogue.md.État vérifié — registre Palomar, 2026-08-30
La réfutation Vibe interprète « le premier banc d’essai exhaustif sera le registre Palomar » comme l’affirmation que Palomar était déjà intégré au dépôt au moment de l’ouverture. Ce n’est pas ce que dit le body : le futur décrit un workstream planifié, non un état courant. L’absence locale alors observée ne réfute donc pas cette phrase.
L’état courant matérialise désormais ce workstream sans transformer Palomar en backlog :
docs/leiden-declaration-position.md, livré surmain, référence cet inventaire et fixe la doctrine : priorité aux propres lakes de CoursIA, apport externe au compte-gouttes seulement ;VEILLEetAUCUNE ACTIONsont des conclusions normales, et une entrée Palomar ne valide jamais un lake entier ;Verdict : RÉFUTATION REJETÉE. La formulation initiale était prospective et exacte ; elle possède aujourd’hui un inventaire et une doctrine vérifiables, mais l’Epic reste ouvert.