EPIC: Digestion et exposition des preuves du corpus CoursIA #13105

Rôle de cet Epic

Cet Epic est d’abord une doctrine de production et d’exposition pour les mathématiques déjà présentes dans CoursIA. Il informe la façon dont nous concevons, relisons et présentons nos lakes, preuves, notebooks et résultats computationnels. Il ne donne pas au dépôt une nouvelle mission d’absorption générale de la littérature formalisée.

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.

Le positionnement de CoursIA face à la Déclaration de Leiden fournit la caution épistémique de cette discipline : certitude et compréhension, attribution, transparence, revue humaine et autonomie ne se réduisent pas à un build vert.

CoursIA possède déjà des cas utiles, notamment 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 cherche d’abord à améliorer la lisibilité et la transmission du corpus existant, puis à faire de cette exigence une habitude pour les futurs résultats produits dans le dépôt.

Frontière de périmètre — HARD

• Priorité 1 : corpus CoursIA existant. Lakes propres, preuves déjà intégrées, notebooks compagnons, traces utiles du prover et résultats computationnels du dépôt.
• Priorité 2 : futurs résultats CoursIA. La grille s’applique au fil de leur création ou d’une révision substantielle ; elle n’impose pas un backfill uniforme immédiat.
• Extension ponctuelle : résultats externes. Un résultat Palomar ou issu d’une autre source ne rejoint le dépôt qu’au compte-gouttes, lorsqu’un besoin pédagogique ou scientifique CoursIA préexistant le justifie.
• Interdit : rollout d’ingestion. L’inventaire Palomar Palomar: inventaire de veille des 68 résultats et raccords CoursIA #13107 n’est ni une queue de dispatch, ni une obligation d’import, ni un mandat de créer de nouveaux parcours. VEILLE et AUCUNE ACTION sont les verdicts normaux de la majorité des entrées.
• Pas de submersion documentaire. La grille guide la conception et la review ; elle ne demande pas un rapport séparé pour chaque preuve. Les findings actionnables deviennent des issues ciblées, jamais des audits committés en série.

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 de digestion

Lorsqu’une preuve ou un résultat CoursIA fait l’objet d’une création ou d’une révision substantielle, documenter à proportion de son importance :

1. l’énoncé exact et le niveau de garantie ;
2. la provenance, la littérature, la priorité et l’attribution ;
3. la nouveauté réelle par rapport aux dépendances ;
4. la carte des dépendances, toolchain, axiomes et hypothèses nommées ;
5. les portions triviales condensées et les portions nouvelles ou difficiles développées ;
6. la friction naturelle : obstacles, pivots, choix, essais ratés utiles et dette résiduelle ;
7. le chemin de découverte, distingué de la reconstruction finale ;
8. les limites, claims non établis et réserves de review ;
9. le raccord au corpus CoursIA et les prérequis ;
10. la transmission : exemple calculé, visualisation ou exercice, plus une revue humaine nommée lorsque la portée le justifie.

Cette grille est proportionnée, non bureaucratique : un lemme local n’appelle pas dix sections artificielles. En revanche, un lake, un grand théorème, une preuve générée par agent ou un notebook de digestion doit rendre ces dimensions visibles. Un inventaire de théorèmes, un certificat seul ou une prose fluide sans carte de difficulté ne suffisent pas.

Ordre de travail

Axe A — audit rétroactif de notre propre corpus

Sous-grain bloquant : #13121.

• Couvrir 100 % des ensembles de preuves propres, portés ou agrégés par CoursIA au grain lake/module substantiel ↔ notebook/compagnon, jamais au grain lemme.
• Classifier les racines en production CoursIA, portage/digestion, agrégateur, vendored/externe ou doublon/miroir.
• Auditer séparément validité formelle, consolidation/canonicalisation et exposition pédagogique.
• Identifier la source canonique, les doublons, la provenance, le niveau de garantie, le compagnon pédagogique et la friction déjà conservée.
• Approfondir uniquement les cas où le triage révèle un écart ; reconnaître les cas conformes sans churn.
• Publier la matrice dans Audit rétroactif: digestion, canonicalisation et exposition des preuves CoursIA #13121 et transformer les findings actionnables en issues ciblées, jamais en rapports committés.
• Comparer Sendov, Analysis I et PFR comme baselines de formes différentes, sans modifier leurs notebooks en l’absence de finding précis.
• Exploiter les traces déjà conservées par le prover (partial_progress, objectifs résiduels, échecs et hints) lorsqu’elles éclairent réellement le chemin de découverte.
• Relier les revues substantielles au registre éditorial existant plutôt que créer une seconde bureaucratie parallèle.

Axe B — incorporer la discipline au travail futur

• Pour tout nouveau lake ou résultat majeur CoursIA, séparer explicitement validité formelle, exposition pédagogique et niveau de maturité.
• Conserver les choix intermédiaires et échecs instructifs sans transformer le notebook en journal brut.
• Exiger une attribution et une carte des dépendances proportionnées au claim.

Axe C — extensions externes choisies

• Utiliser Palomar: inventaire de veille des 68 résultats et raccords CoursIA #13107 comme référence de veille, non comme backlog.
• N’ouvrir un grain Palomar que si un parcours CoursIA existant formule d’abord le besoin.
• Préférer un raccord narratif ou une non-action à un import sans ancrage.
• Commencer, si un besoin réel se confirme, par un seul pilote ; réévaluer avant toute extension supplémentaire.

Critères d’acceptation

• L’audit Audit rétroactif: digestion, canonicalisation et exposition des preuves CoursIA #13121 couvre 100 % des ensembles de preuves propres/portés/agrégés ; le dénominateur final et les exclusions sont explicités.
• Chaque ensemble distingue validité formelle, consolidation/canonicalisation et exposition pédagogique.
• Au moins trois cas internes non conformes sont approfondis lorsqu’ils existent ; si moins de trois écarts survivent au triage, les cas conformes sont conservés sans churn.
• Au moins un cas montre comment une preuve interne gagne en exposition sans changer son contenu mathématique.
• Au moins un cas conserve explicitement un chemin de découverte ou un échec instructif déjà disponible dans nos traces.
• La distinction validité formelle / exposition / maturité est visible dans la review des futurs résultats majeurs.
• Toute extension externe livrée répond à un besoin CoursIA préexistant et reste atomique.
• Aucun seuil d’import Palomar, nombre de notebooks externes ou campagne exhaustive n’est requis pour fermer l’Epic.
• Une synthèse transverse relie les cas internes sans proclamer une canonicalisation achevée sur la seule base d’un build vert.

Références

• Terence Tao, Mathematics in the Age of AI, ICM 2026, arXiv:2608.16753.
• Leiden Declaration on AI and Mathematics, 2 juin 2026, DOI 10.5281/zenodo.20302944.
• Positionnement CoursIA–Leiden : PR docs(ethics): position CoursIA on Leiden declaration #13112.
• Inventaire de veille Palomar : Palomar: inventaire de veille des 68 résultats et raccords CoursIA #13107.
• Epic précédent : EPIC: Terry Tao 2026 — digestions Lean (Sendov phase 1, Analysis phase 2) #10763.
• Précédents CoursIA : docs/grothendieckian-lens.md et docs/magnifica-humanitas-dialogue.md.