CoursIA face à la Déclaration de Leiden

Statut de ce texte

La Déclaration de Leiden sur l’intelligence artificielle et les mathématiques a été publiée le 2 juin 2026, déposée sous le DOI 10.5281/zenodo.20302944 et endossée par l’International Mathematical Union. Elle est issue d’un groupe de travail réuni au Lorentz Center en septembre 2025.

Ce document n’est ni une paraphrase de la Déclaration, ni une déclaration d’adhésion sans réserve. Il situe CoursIA face à ses valeurs, confronte ces valeurs à des artefacts vérifiables du dépôt et nomme les écarts qui restent ouverts. Il suit en cela deux précédents du projet : le dialogue avec Magnifica Humanitas, qui répond à un texte externe par des objets concrets, et la clé de lecture grothendieckienne, qui conserve les changements de cadre, les échecs et les niveaux de certification.

Le texte est daté. Un workflow, un registre ou un notebook cité ici peut évoluer ; le lien vers l’artefact prime sur la déclaration de conformité.

Notre lecture de Leiden

Leiden protège cinq choses que l’usage de l’IA rend plus faciles à dissocier :

  1. la pluralité des motivations mathématiques, avec la preuve comme niveau élevé de certitude ;
  2. l’attribution à des auteurs identifiables, responsables de leurs résultats ;
  3. la transparence des arguments et leur vérification indépendante ;
  4. l’évaluation partagée de la profondeur, de la difficulté et de l’importance ;
  5. la compréhension, le jugement et l’autonomie dans le choix des questions.

La Déclaration alerte symétriquement sur cinq menaces : arguments plausibles mais faux, exploitation du corpus et défaut d’attribution, distorsion des incitations, communication contournant la revue communautaire, et dépendance industrielle susceptible de déplacer les priorités de recherche.

CoursIA partage ce diagnostic, avec une précision issue de son expérience : la validité technique et la valeur pédagogique sont deux axes distincts. Un notebook peut s’exécuter de bout en bout et mal expliquer son objet. Une preuve Lean peut être acceptée par le noyau et rester opaque, mal attribuée ou dépendante d’axiomes non discutés. À l’inverse, un récit limpide ne compense jamais un résultat non reproduit.

Cette distinction motive l’Epic de digestion et exposition des preuves du corpus CoursIA, inspiré de la chaîne proposée par Terry Tao dans Mathematics in the Age of AI : génération, vérification, exposition, publication, puis digestion dans un corpus humainement cohérent.

Cet Epic est une discipline interne avant d’être une politique d’acquisition : il s’applique d’abord aux lakes, preuves et notebooks que CoursIA possède déjà, puis aux futurs résultats produits dans le dépôt. Il ne transforme ni Leiden ni Palomar en mandat d’étendre indéfiniment le périmètre scientifique de CoursIA. Les résultats externes ne sont considérés qu’au compte-gouttes, lorsqu’un besoin pédagogique préexistant les appelle.

La Boussole : de l’interprétation à la preuve formelle

L’Epic #13105 se déploie selon un parcours en trois temps — apprendre, extraire, prouver — que la littérature récente de l’interprétabilité mécaniste et de la formalisation permet aujourd’hui de nommer et de relier. Cette Boussole n’est pas un programme nouveau : c’est une lecture transverse de ce que CoursIA fait déjà, articulée pour qu’un lecteur extérieur puisse en suivre le fil sans avoir à reconstituer les épisodes.

Apprendre. Le grokking observé par R02 (Power, Burda, Edwards, Babuschkin et Misra, 2022, arXiv:2201.02177 — phase tardive où un réseau dépasse la mémorisation et accède à une structure algorithmique) montre qu’un modèle peut converger au-delà de ses performances d’entraînement. Pour CoursIA, ce temps correspond à la phase d’accumulation disciplinée des notebooks, des preuves et des lakes — sans garantie que la performance finale en soit lisible.

Extraire. R03 (Michaud et al., 2024, arXiv:2402.05110 — program synthesis via mechanistic interpretability) montre qu’à partir d’un réseau grokké, on peut extraire un programme lisible. Côté CoursIA, ce geste est porté par les organes d’interprétabilité (harnais SAE Qwen, #10355), par les notebooks d’AST et de circuits, et par les passages qui reconstruisent un algorithme identifiable à partir d’un artefact neuronal. L’extraction n’est pas seulement technique : elle exige de choisir le niveau d’abstraction où le programme devient lisible par un humain, et ce choix est pédagogique avant d’être mathématique.

Prouver. R15 (Bursuc, Ehrenborg, Lin et al., 2025, arXiv:2509.22908 — vericoding), démontre que la sortie d’un modèle peut être accompagnée d’une preuve formelle vérifiée par un noyau. La chaîne Tao Mathematics in the Age of AI propose précisément ce contrat : génération, vérification, exposition, puis digestion dans un corpus humainement cohérent. Lean-18 Sendov, Lean-19 Analysis I et Lean-20 PFR sont trois premières mailles locales de cette chaîne.

Les deux directions de l’intersection. La Boussole distingue deux usages distincts de la preuve formelle appliquée à l’IA :

  • Prouver des réseaux — montrer qu’une propriété d’un modèle tient (robustesse, équité, absence de porte dérobée). R12 (Towards Guaranteed Safe AI, Dalrymple et al., 2024, arXiv:2405.06624, distillé dans #17216) trace cette direction et la relie à la triade world/solver/verifier.
  • Utiliser l’IA pour prouver — outiller la formalisation elle-même. Notre chaîne Epic #13105 vit ici : Lean comme cible, agents et notebooks comme exposants.

Ces deux directions ne sont pas séparables : un verifier qui s’appuie sur du Lean gagné par un modèle est exposé aux mêmes questions d’attribution qu’un réseau dont on prouve la correction.

Questions ouvertes que la Boussole ne tranche pas.

  • Échelle — jusqu’où la vérification formelle reste-t-elle lisible quand le modèle et la preuve grandissent ensemble ? La lecture de Sendov ou de PFR tient parce que le périmètre reste borné ; le seuil où la preuve cesse d’être un cours est empirique et non garanti.
  • Réduction symbolique — l’extraction par R03 produit un programme MIPS lisible, mais la translation vers une théorie de bibliothèques (Mathlib, PFR) reste un travail humain. L’écart entre extraction et digestion est précisément le périmètre de l’Epic #13105.
  • Niveau d’understanding — qu’est-ce qu’une preuve formelle comprise ? La Boussole distingue la validité du noyau (technique) et la lisibilité du récit (pédagogique) ; elle ne prétend pas les confondre.
  • Prouver l’absence de capacités — c’est la question inverse de la triade W/S/V, et la plus difficile : on prouve plus facilement la présence d’une capacité (par témoin) que son absence.

Sources principales de la Boussole (archivées au gisement partagé, jamais committées) :

  • R01 — AI Feynman 2.0 — Pareto-optimal symbolic regression exploiting graph modularity (arXiv:2006.10782) · sha8 F01E25E3
  • R03 — Opening the AI black box — program synthesis via mechanistic interpretability (arXiv:2402.05110) · sha8 690A0E86
  • R10 — Not All Language Model Features Are One-Dimensionally Linear (arXiv:2405.14860) · sha8 7DEAC929
  • R12 — Towards Guaranteed Safe AI (arXiv:2405.06624), distillation #17216
  • R14 — Open Problems in Mechanistic Interpretability (arXiv:2501.16496) · sha8 9A50CDC6
  • R15 — A benchmark for vericoding (Bursuc, Ehrenborg, Lin et al., 2025, arXiv:2509.22908)
  • Terry Tao, Mathematics in the Age of AI, ICM 2026 (arXiv:2608.16753)

Principes, pratiques, preuves et engagements

Principe de Leiden Pratique CoursIA actuelle Preuve consultable Lacune reconnue Engagement
La preuve vise certitude et compréhension Les notebooks combinent exécution, narration, exemples et exercices ; les preuves Lean sont relues au-delà du simple build Règles de validation H.1–H.7, discipline de review Lean, série Lean Un build vert ne mesure ni la lisibilité ni la digestion Appliquer d’abord la grille de l’Epic #13105 aux résultats existants de CoursIA où l’écart d’exposition est vérifié, puis aux futurs résultats majeurs au fil de leur création
Attribution et responsabilité humaines Les sources, auteurs et artefacts amont doivent être nommés ; une attribution douteuse bloque une conclusion Verify Before Claiming, registre d’attribution MBML, anti-régression La provenance n’est pas encore uniforme dans tous les notebooks historiques Traiter chaque lacune actionnable par une issue dédiée, avec source primaire et correction vérifiable
Transparence et vérification indépendante Outputs réels committés, exécution end-to-end, comptage des axiomes et validation après modification Règles notebooks, couverture proof-integrity, PARCOURS La couverture proof-integrity n’atteint pas encore tous les lakes Étendre la couverture sans présenter les lakes non câblés comme déjà certifiés
Standards partagés d’évaluation Les axes éditorial, reproductibilité et revue scientifique sont séparés ; les reviews substantielles sont enregistrées PARCOURS, registre de revues éditoriales, carte de revue Les registres restent partiels et la qualité pédagogique garde une part de jugement humain Nommer la portée de chaque review et refuser l’auto-promotion par métrique unique
Compréhension, jugement et autonomie Le dépôt privilégie les outils ouverts, locaux ou reproductibles lorsque c’est possible ; les limites des services externes sont documentées Services GenAI, matrice de coût, politique de taille et reproductibilité Modèles, GPU, APIs et plateformes cloud créent encore des dépendances réelles Rendre chaque dépendance visible et distinguer RECOVERABLE-* d’une impossibilité intrinsèque
Ouverture et partage Notebooks, scripts, preuves et sorties pédagogiques sont versionnés dans le dépôt ; les données et licences sont inventoriées Registre datasets, THIRD_PARTY_NOTICES, politique SOTA Ouverture du code ne signifie pas gratuité énergétique, accès universel aux modèles ou licence uniforme des sources Publier les coûts, licences et prérequis au même niveau que les résultats

Ce que nos artefacts démontrent — et ce qu’ils ne démontrent pas

1. Exécution authentique

CoursIA exige que les notebooks committés conservent leurs sorties et que toute cellule de code modifiée soit ré-exécutée. Cette règle combat une forme directe de plausible-but-false : un récit qui affirme un résultat que le livrable ne produit pas. Elle interdit aussi de maquiller manuellement une sortie ; la cause doit être corrigée puis l’exécution rejouée.

Cette discipline démontre qu’une sortie a été produite dans un environnement donné. Elle ne démontre pas, à elle seule, que l’expérience répond à la bonne question, que le problème n’est pas dégénéré ou que l’interprétation est juste. Les critères de validation réelle et de vrai outil SOTA existent précisément pour éviter ce glissement.

2. Vérification formelle

Les lakes Lean permettent d’interroger les axiomes, de construire les modules et, lorsque le workflow est câblé sur la cible, de contrôler l’intégrité des preuves. CoursIA distingue explicitement sorryAx, native_decide.* et Classical.choice plutôt que de réduire la confiance à l’absence textuelle de sorry.

Cette précision reste incomplète : la carte de couverture montre que tous les lakes ne sont pas atteints par le même gate. Un succès hors cible n’est donc jamais présenté comme une preuve sur cible.

3. Exposition et digestion

Lean-18 Sendov, Lean-19 Analysis I et Lean-20 PFR illustrent trois formes de digestion : exposer un grand résultat, étudier un workflow de formalisation et relier une méthode entropique à un lake réel. Ces notebooks sont des points de départ, pas des certificats de canonicalisation définitive.

L’inventaire de veille Palomar rend cette prudence opérationnelle. Au snapshot du 26 août 2026, le registre comptait 68 résultats actifs et 76 versions. Un seul résultat, Sendov, avait un chevauchement direct avec une digestion CoursIA existante. La plupart des autres reçoivent VEILLE ou AUCUNE ACTION : être vérifié dans Palomar ne suffit pas à justifier un import, un notebook ou une place dans le curriculum. Cet inventaire n’est pas un backlog ; il ne devient actionnable qu’en réponse à un besoin déjà formulé par un parcours CoursIA.

4. Revue humaine

Le registre de revues éditoriales refuse qu’un notebook soit promu par simple ancienneté ou auto-évaluation. La portée de la review — typographie, faits, pédagogie, substance ou revue complète — est nommée.

Le registre ne prétend pas couvrir tout le dépôt. Il constitue un mécanisme de responsabilité, non une preuve que tout artefact absent serait mauvais ou que tout artefact présent serait définitif.

Cinq menaces confrontées au dépôt

Arguments plausibles mais faux

La réponse ne peut pas être seulement stylistique. CoursIA combine exécution, sorties réelles, contrôles de régression, tests, revue du diff et, pour Lean, inspection des axiomes. Les règles Verify Before Claiming et Audit Reassessment imposent de confronter les verdicts automatisés au code réel, car un audit peut lui-même produire un faux positif.

Risque résiduel : un check peut être vert tout en mesurant le mauvais objet. Le dépôt conserve plusieurs études de cas de ce phénomène dans Quand la vérification est verte et le système est cassé.

Exploitation du corpus et mauvaise attribution

Les datasets, sources pédagogiques, lakes et logiciels tiers doivent être reliés à leur provenance et à leur licence. L’usage d’un modèle n’efface pas les auteurs des données ou des preuves dont il dépend.

Risque résiduel : les notebooks historiques n’ont pas tous le même niveau de détail bibliographique. L’engagement est de corriger les manques vérifiés, sans inventer une priorité ou conclure à l’absence d’antériorité depuis une recherche négative rapide.

Distorsion des incitations

Un nombre de preuves, de PRs, de cellules ou de notebooks n’est pas une mesure suffisante du progrès. Le protocole de variation sépare contenu et méta-outillage et exige qu’un cycle ajoute quelque chose qu’un lecteur ou un étudiant puisse utiliser.

Risque résiduel : toute métrique peut devenir une cible. Les tags DEEP/MED/LIGHT, les densités et les gates restent des instruments de triage ; la décision se relit contre le livrable.

Communication qui contourne la revue

CoursIA ne traite pas une annonce de blog, une fiche de registre ou un résultat de modèle comme un substitut à la source et à la revue. Pour une PR ou une issue, le body complet, les commentaires, les reviews et le diff sont lus avant décision.

Risque résiduel : la vitesse de production peut dépasser la capacité de revue. L’Epic #13105 nomme cette situation « indigestion de preuve » et privilégie l’exposition, l’attribution et l’intégration au corpus plutôt que l’accumulation de certificats.

Dépendance industrielle et perte d’autonomie

Le dépôt utilise des services commerciaux, des modèles propriétaires et des plateformes cloud, mais maintient aussi des environnements locaux, des scripts reproductibles et des alternatives ouvertes. L’autonomie est évaluée capacité par capacité, jamais proclamée globalement.

Risque résiduel : le matériel, les licences, les tokens, les modèles gated et les coûts énergétiques limitent encore l’accès. Un fallback dégradé n’est pas consacré comme résultat SOTA lorsqu’un chemin de réparation existe.

Tensions que nous refusons de lisser

Vitesse contre revue

L’IA réduit le coût de génération. Elle ne réduit pas automatiquement le coût de vérification sémantique, d’attribution, d’exposition ou de maintenance. Lorsque le flux dépasse la revue, ralentir la publication peut constituer le progrès responsable.

Formalisation contre compréhension

La formalisation rend des hypothèses et des dépendances inspectables. Elle peut aussi déplacer l’opacité vers les bibliothèques, les tactiques, les ponts de langage ou la sélection même de l’énoncé. Une preuve noyau-correcte n’est pas encore un cours.

Ouverture contre coût

Versionner les sorties et les dépendances améliore la reproductibilité, mais augmente la taille du dépôt, le temps de CI et l’empreinte de calcul. La politique de taille assume ce compromis et demande de mesurer le coût plutôt que de l’effacer.

Infrastructure locale contre dépendances

L’auto-hébergement augmente le contrôle et la réparabilité, sans supprimer les dépendances aux fabricants, aux modèles et aux communautés open source. Le verdict honnête se formule par composant.

Reconstruction claire contre chemin de découverte

Une exposition finale doit être lisible. Mais supprimer tous les essais ratés, pivots et choix intermédiaires rend la difficulté invisible et l’apprentissage plus pauvre. La digestion conserve une sélection d’échecs instructifs, sans transformer le notebook en journal brut.

Engagements CoursIA

  1. Disclosure situé. Nommer l’usage d’IA lorsqu’il affecte la génération, la vérification, l’exposition ou la décision scientifique ; ne pas réduire ce disclosure à une signature générique.
  2. Responsabilité humaine finale. Une sortie de modèle, un verdict de bot ou un build vert ne décide jamais seul de la justesse d’un claim.
  3. Attribution active. Chercher et citer les sources primaires, les auteurs, les dépôts substantifs et les licences ; distinguer un wrapper du travail qu’il enveloppe.
  4. Preuve inspectable. Publier, lorsque le domaine le permet, toolchain, dépendances, axiomes, seeds, paramètres, sorties et limites.
  5. Outputs authentiques. Corriger la cause puis ré-exécuter ; ne jamais hand-éditer une sortie pour la rendre plus propre ou conforme au récit.
  6. Revue nommée. Documenter qui a relu quoi, avec quelle portée ; éviter que « reviewed » devienne un label sans contenu.
  7. Résultats négatifs conservés. Garder les non-reproductions, réfutations et plafonds lorsqu’ils changent la décision scientifique.
  8. Digestion interne avant accumulation ou ingestion. Améliorer d’abord l’exposition des résultats déjà produits par CoursIA et intégrer cette exigence au travail futur ; n’ajouter un résultat externe qu’en réponse à un besoin pédagogique préexistant, jamais pour remplir un quota d’imports.
  9. Autonomie mesurée. Favoriser les outils ouverts et locaux sans masquer les dépendances restantes.
  10. Coûts visibles. Documenter les coûts de calcul, d’accès et d’énergie lorsqu’ils conditionnent la reproductibilité ou l’équité d’accès.

Ce que nous ne revendiquons pas

  • Un build Lean ne certifie ni la nouveauté, ni l’importance, ni la pédagogie d’un résultat.
  • Une exécution Papermill ne certifie pas que l’expérience est non triviale ou que son interprétation est correcte.
  • Une entrée Palomar ne valide pas un lake entier et n’impose pas son import.
  • L’inventaire Palomar ne donne pas à CoursIA une mission générale d’ingestion des mathématiques formalisées.
  • L’Epic de digestion n’impose ni audit uniforme de chaque lemme, ni rapport séparé pour chaque preuve, ni backfill immédiat de tout le corpus.
  • Un modèle local ne rend pas l’infrastructure indépendante de toute industrie.
  • Un dépôt public ne résout pas les barrières de matériel, de licence ou d’énergie.
  • Une grille de review ne remplace pas le jugement mathématique et pédagogique.
  • Ce document ne constitue pas une canonicalisation achevée ; il énonce des engagements vérifiables et des lacunes ouvertes.

Dialogue avec les recommandations de Leiden

Aux mathématiciens, Leiden demande disclosure, attribution, revue, responsabilité et formation continue. CoursIA répond par des règles d’exécution et de review, mais doit encore homogénéiser la provenance historique.

Aux organisations et financeurs, Leiden demande des standards de publication, la protection des auteurs, des infrastructures publiques et le maintien de la rigueur. CoursIA peut documenter des pratiques et fournir des artefacts ouverts ; il ne possède ni l’autorité d’un journal ni celle d’un financeur.

Aux pouvoirs publics, Leiden recommande de protéger les auteurs, de résister au battage promotionnel, de réguler l’industrie et d’investir dans des infrastructures publiques. CoursIA peut rendre visibles les dépendances et les coûts, non se substituer à cette politique.

À l’industrie, Leiden demande le respect des standards communautaires, de l’autonomie et des préoccupations éthiques. CoursIA évalue les outils par leurs résultats et leurs conditions d’usage, et refuse de transformer l’accès à un service en preuve de neutralité ou de légitimité.

Accord avec l’initiative SAIR Open Models

L’initiative SAIR Open Models (page consultée le 24 septembre 2026) appelle la communauté mathématique à construire des modèles ouverts « shaped by the community » pour l’âge de l’IA en mathématiques. Sa première phase annoncée concerne « le travail mathématique quotidien : comprendre des arguments difficiles, vérifier des références, explorer des exemples, écrire du code, et formaliser des preuves » (sair.foundation/open-math-model/, section Tools for Everyday Research). L’initiative fixe cinq principes — poids, code et méthodes d’entraînement publiés, données aux sources documentées et aux permissions compatibles, licences ouvertes (Apache 2.0, MIT, CC BY 4.0), gouvernance publique, indépendance de recherche préservée face aux partenaires industriels — et reconnaît que des précisions détaillées sont attendues « dans un avenir très proche ».

CoursIA partage la direction de ces principes, avec une portée volontairement bornée. Le mainteneur du dépôt s’y est inscrit comme soutien de l’initiative. Cette inscription n’établit ni partenariat, ni financement, ni rôle de gouvernance ; elle reconnaît une convergence d’intentions que nos artefacts vérifiables peuvent rendre concrète.

Correspondances avec nos engagements

  • Ouverture contre coût. L’initiative demande que les poids, le code et les évaluations soient publiés et reproductibles (open-math-model, Open Development). CoursIA tient le même engagement par ses notebooks versionnés, ses proofs vérifiables (lake build + proof-integrity) et ses sorties pédagogiques committées. La politique de taille assume explicitement que cette ouverture augmente le coût de calcul et de stockage : le compromis est mesuré, jamais effacé.
  • Données aux sources documentées. L’initiative exige que les données d’entraînement viennent avec des sources et permissions compatibles, et que les utilisateurs consentent explicitement à tout usage (open-math-model, The Mathematical Community Owns the Data). CoursIA rejoint ce principe par le registre de datasets, par le registre d’attribution MBML, et par la règle Verify Before Claiming qui refuse les attributions extrapolées.
  • Licences ouvertes. L’initiative cite Apache 2.0, MIT et CC BY 4.0 (open-math-model, Shared Intellectual Property). Les dépendances du dépôt sont inventoriées dans THIRD_PARTY_NOTICES et la règle bibliography-hygiene refuse le commit de publications sous droits.
  • Gouvernance publique et indépendance de recherche. L’initiative énonce que la communauté mathématique doit gouverner l’initiative, et que les partenariats industriels doivent préserver l’indépendance de recherche (open-math-model, Open Community and Governance). CoursIA traduit ce principe par son inscription comme soutien — pas comme financeur, contributeur de calcul, ou membre d’un comité — et par sa séparation explicite entre dépendance industrielle et autonomie (Engagement 9 — Autonomie mesurée).
  • Infrastructure locale contre dépendances. L’initiative demande que les modèles soient exécutables indépendamment (open-math-model, Models Shaped by the Community). Le dépôt héberge localement les poids ouverts lorsque c’est possible et documente ses dépendances cloud ou propriétaires par composant.

Contribution vérifiable

L’accord avec SAIR est rendu concret par deux pratiques déjà tenues dans le dépôt :

  • Les lakes Lean servent d’évaluations reproductibles. Quand un workflow lake build est câblé et que proof-integrity est vert sur la cible, le résultat est inspectable par quiconque dispose de la toolchain. La carte de couverture rend cette discipline explicite et évite de présenter des lacs non câblés comme déjà certifiés.
  • Le harnais de prouveur et ses traces forensiques (Epic #1453) tiennent un journal des tentatives, des succès et des plafonds sur petits modèles. Cette pratique alimente la Boussole et donne à l’accord un contenu vérifiable plutôt qu’une déclaration de principe.

Ce que nous ne revendiquons pas

  • Aucun partenariat formel avec l’initiative ; aucune mission de représentation, de gouvernance ou de financement.
  • Aucune contribution de calcul, de données, ou de personnel au-delà de l’apport de cet accord documenté.
  • Aucun alignement sur des décisions futures de l’initiative qui n’auraient pas encore été publiées ; la page consultée annonce elle-même des précisions « dans un avenir très proche » et l’accord est daté du 24 septembre 2026.
  • Aucun ajout de SAIR Open Models au périmètre pédagogique ou scientifique de CoursIA au-delà de la formalisation déjà tenue dans les lakes ; Epic #13105 demeure une discipline interne avant d’être une politique d’acquisition.
  • Aucun usage de cet accord comme preuve de neutralité, d’a-completude ou de supériorité face à d’autres initiatives ouvertes.

Sources principales

Retour au sommet