Au-delà du lycée : démonstration, entraînement olympique et mathématiques de niveau doctorat — ce que le « mode Doctorat » pourrait réalistement contenir

Résultats

(a) Le cours de transition vers la démonstration et la recherche sur l’enseignement de la démonstration

La plupart des départements américains insèrent un cours de « transition vers la démonstration » entre le calcul différentiel et intégral et le premier cours réellement axé sur la démonstration (algèbre, analyse réelle) [1]. Sa pédagogie dominante est la méthode Moore : l’enseignant ne donne que des axiomes et une liste de problèmes séquencée ; les étudiants ne peuvent pas consulter de manuels, doivent tout démontrer eux-mêmes, et présentent leurs résultats les uns aux autres [1][2]. Les preuves de son efficacité sont surtout qualitatives et de long terme (davantage d’étudiants s’orientant vers la recherche) plutôt que rigoureusement quantitatives [2].

La recherche de Selden & Selden établit une distinction centrale pour la conception de l’évaluation : la construction de démonstration et la validation de démonstration (juger si l’argument d’autrui est correct) sont des compétences distinctes, et un cours centré sur la construction n’améliore pas de façon fiable la validation [3][4]. Les études par suivi oculaire et verbalisation à voix haute montrent que les novices se fixent sur des traits superficiels (manipulation algébrique) tandis que les experts suivent la structure logique globale ; la validation est présentée comme une construction de sens active, pas une vérification binaire — ce qui explique précisément pourquoi elle résiste à une grille appliquée par une machine [3][4].

La gestion des quantificateurs est le domaine d’échec le plus répliqué : une étude portant sur 61 étudiants a trouvé qu’aucun ne pouvait réécrire de façon cohérente un énoncé informel en son équivalent formel quantifié correct [1]. Modes d’échec récurrents : ne pas introduire de variable en démontrant un énoncé universel ; sur-attribuer des propriétés à un témoin existentiel ; échanger l’ordre des quantificateurs (classique dans les démonstrations ε-δ) ; et mal nier un énoncé (énoncer « l’opposé » plutôt que la négation logique), ce qui compromet la démonstration par l’absurde [5][6]. Une étude en algèbre linéaire a de même trouvé des étudiants qui « se parlaient sans se comprendre » sur des sens différents du mot « unique » [6]. Ce sont des modes d’échec discrets et bien définis — chacun ciblable par un exercice étroit et vérifiable (voir Implications pour la conception).

(b) Comment fonctionne l’entraînement olympique

L’entraînement olympique s’organise autour d’heuristiques + une banque de techniques, pas un programme linéaire. How to Solve It de Pólya (1945) fournit l’heuristique en quatre étapes — comprendre, planifier, exécuter, revoir — qui sous-tend essentiellement toute la littérature d’entraînement à la compétition [7][11]. Problem-Solving Strategies d’Engel (Springer, 1998), destiné aux entraîneurs jusqu’au niveau IMO/Putnam, s’organise par technique (invariants, principe des tiroirs, principe extrémal, induction, coloriage/dénombrement) plutôt que par sujet MSC [10][11].

AoPS met cela en œuvre à grande échelle — les problèmes avant les explications, des programmes allant de la préalgèbre jusqu’à MATHCOUNTS/AMC/AIME/ARML et WOOT (entraînement olympique) ; chaque membre de l’équipe américaine à l’IMO depuis 2015 a été étudiant d’AoPS [8]. La préparation au Putnam suit le même modèle piloté par des ensembles de problèmes, renforcé par des séances de groupe façon séminaire [9][11].

La notation, dans les deux cas, est délibérément grossière et non additive — un rejet de la notation point par étape. Les problèmes de l’IMO sont notés de 0 à 7, évalués soit « en partant de 7 vers le bas » (quasi complet), soit « en partant de 0 vers le haut » (idée cruciale manquante) ; le crédit partiel reflète la progression conceptuelle, pas le nombre de lignes [23][24]. Le Putnam utilise une échelle de 0 à 10, mais en pratique seules les notes zéro, un, deux, huit, neuf et dix sont attribuées — le « Gap of Death » (l’écart entre 3 et 7) est presque jamais utilisé, si bien qu’une démonstration à laquelle il manque la pleine rigueur obtient ≤2 quel que soit le travail d’apparence correcte qui l’entoure [12]. C’est un signal direct que le crédit partiel jugé par un humain sur des démonstrations résiste à toute grille mécanique additive — le même écart que les correcteurs automatiques ne parviennent toujours pas à combler (partie d).

(c) La taxonomie thématique des mathématiques avancées et les examens de qualification du doctorat

La Classification thématique des mathématiques (MSC 2020), maintenue conjointement par l’AMS/MathSciNet et zbMATH, est ce qui se rapproche le plus d’une taxonomie officielle de l’ensemble des mathématiques : 63 codes principaux à deux chiffres, de 00 Général et 03 Logique jusqu’à la famille de l’algèbre (12-20), la famille analyse/géométrie/topologie (26-58), probabilités/statistiques (60-62), les domaines appliqués (68 informatique, 76-86 mécanique, 90-94 recherche opérationnelle/théorie des jeux/information), jusqu’à 97 Didactique des mathématiques [15][16]. Chaque code se subdivise en domaines de second niveau désignés par des lettres [15].

Les examens de qualification du doctorat échantillonnent un socle restreint et assez universel plutôt que l’ensemble des 63 domaines. Harvard en nomme six : algèbre (Sylow, anneaux/modules, Galois, théorie des représentations), géométrie algébrique (variétés, Riemann-Roch), analyse complexe (théorie de Cauchy, résidus, surfaces de Riemann), topologie algébrique (groupe fondamental, (co)homologie, dualité de Poincaré), géométrie différentielle (variétés, fibrés, courbure), et analyse réelle (théorie de la mesure, espaces Lp, analyse de Fourier, EDP, probabilités, espaces de Sobolev) [13]. D’autres établissements (TCU, UNT, Stanford, Penn State) exigent 2 à 4 examens tirés d’un menu similaire mais plus restreint — ce qui confirme que « niveau doctorat » signifie de la profondeur sur une poignée de piliers centraux, pas une couverture encyclopédique de la MSC [14].

(d) Formats évaluables automatiquement pour les mathématiques avancées

STACK (Moodle, adossé au système de calcul formel Maxima) et WeBWorK (langage « PG » en Perl) sont les deux systèmes matures et largement déployés pour la vérification de réponses numériques/symboliques : les deux valident la saisie, vérifient l’équivalence algébrique (pas une correspondance de chaîne) via des paramètres aléatoires par étudiant, et donnent une rétroaction instantanée — aucun des deux ne prétend noter une démonstration écrite [17][18][19]. La même technique — soustraire, simplifier, vérifier que le reste est symboliquement nul, ou se rabattre sur une évaluation numérique — est ce que les bibliothèques de type SymPy fournissent de façon programmatique, et sous-tend les dispositifs de notation par LLM mathématiques contemporains [25].

Pour la notation d’une véritable démonstration, la seule approche mécaniquement solide est un assistant de preuve : Lean 4 + mathlib compile une démonstration et l’accepte ou la rejette — pas de crédit partiel, mais une ambiguïté nulle [20]. Le Natural Number Game (Imperial College London) démontre que cela fonctionne comme produit pédagogique, en gamifiant les axiomes de Peano de sorte que des faits « évidents » comme a+b=b+a doivent être prouvés à un compilateur ; « Mathematics in Lean » étend l’idée au contenu de premier cycle universitaire [20][21].

Noter les démonstrations en langage naturel — le format que les étudiants écrivent réellement — reste non résolu. LeanTutor (2026) autoformalise une démonstration étape par étape en Lean, mais a besoin d’une solution de référence déjà formalisée [26]. IMO-GradingBench (2025), à partir de 1 000 solutions d’IMO notées par des humains, a trouvé que même les modèles de pointe (o3, Gemini 2.5 Deep Think) n’atteignent que 52-54 % d’accord exact avec les correcteurs humains en aveugle (sans référence), avec des erreurs concentrées dans la distinction entre « partiel » et « faux » ; les humains avec une référence corrèlent à 0,96 [22]. RefGrader (2025) améliore la fiabilité en notant toujours par rapport à une référence plutôt qu’en aveugle, au prix d’avoir besoin de cette référence déjà construite [27]. La notation par IA des démonstrations en langage naturel est réelle mais trop peu fiable à la frontière la plus difficile pour être le seul mécanisme de notation d’une rétroaction instantanée et fiable.

Implications pour la conception de Math Challenge

Filières proposées au-delà du lycée, chacune avec des sujets concrets et — point crucial — un mécanisme de notation automatique honnête et réaliste :

1. Filière U1 — Transition vers la démonstration. Sujets : logique propositionnelle/des prédicats, manipulation des quantificateurs (ordre ∀/∃, négation), démonstration directe, contraposée, induction, démonstration par l’absurde, théorie des ensembles et fonctions de base. Notation automatique : choix multiple/sélection multiple sur « laquelle de ces propositions est la bonne négation de cet énoncé », « insère le quantificateur manquant », et des exercices de classement d’étapes (les lignes d’une démonstration valide sont mélangées, l’étudiant les réordonne) — cela cible directement les échecs documentés sur les quantificateurs et la structure relevés par Selden & Selden et la littérature sur l’ordre des quantificateurs [3][5][6].

2. Filière U2 — La validation de démonstration comme compétence à part entière. Présenter une courte « démonstration » contenant un défaut intégré (mauvais ordre de quantificateurs, étape non justifiée, raisonnement circulaire) et demander à l’étudiant de sélectionner la ligne exacte qui pose problème, ou de classer l’ensemble de l’argument comme valide/invalide/incomplet. Cela découle directement de la découverte de Selden & Selden selon laquelle la pratique de la construction ne se transfère pas à la capacité de validation — cela nécessite son propre type d’exercice [3][4].

3. Filière U3 — Algèbre abstraite (groupes, anneaux, corps). Sujets : axiomes de groupe, théorème de Lagrange, groupes cycliques, homomorphismes/isomorphismes, groupes quotients, théorie de base des anneaux/corps. Notation automatique : réponses numériques/structurelles (ordre d’un élément, cette application est-elle un homomorphisme — oui/non avec un élément contre-exemple requis si non), complétion de table de Cayley, choix multiple sur « quel axiome échoue ici ».

4. Filière U4 — Analyse réelle. Sujets : suites/limites, continuité ε-δ, dérivabilité, intégration de Riemann, critères de convergence de séries. Notation automatique : réponse numérique (trouver N tel que |a_n - L| < ε), choix multiple sur le critère de convergence applicable, et saisie de contre-exemple (« donne une suite qui converge simplement mais pas uniformément ») vérifiée par rapport à une bibliothèque de contre-exemples valides connus, plus un vérificateur symbolique/numérique (évaluer le candidat en des points d’échantillonnage).

5. Filière U5 — Algèbre linéaire au-delà du cours d’introduction. Sujets : valeurs propres/vecteurs propres, diagonalisation, forme de Jordan, espaces à produit scalaire, théorème spectral. Notation automatique : entièrement numérique/symbolique — cette filière est essentiellement gratuite avec un moteur de calcul formel équivalent à SymPy (le modèle STACK/Maxima s’applique presque directement) [17][18].

6. Filière U6 — Combinatoire et théorie des nombres (saveur olympique). Sujets : principe des tiroirs, invariants, arithmétique modulaire, fonctions génératrices, combinatoire extrémale — modelés directement sur la taxonomie d’Engel et la structure AoPS/WOOT [8][10]. Notation automatique : cette filière convient le mieux au modèle existant de Math Challenge — presque tous ces problèmes ont une réponse finale numérique unique ou sous forme close, exactement comme les problèmes à compléter de style AMC/AIME/Putnam, donc aucun nouveau mécanisme de notation n’est nécessaire au-delà de ce que l’échelle fait déjà plus bas.

7. Filière G1 — Topologie. Sujets : espaces métriques/topologiques, compacité, connexité, continuité, bases du groupe fondamental. Notation automatique : choix multiple (« cet espace est-il compact — oui/non, choisis le recouvrement qui échoue »), Vrai/Faux avec sélection de justification (choisir laquelle des 4 justifications candidates est valide), puisque les démonstrations topologiques ouvertes ne sont pas vérifiables mécaniquement sans formalisation.

8. Filière G2 — Théorie de la mesure et analyse réelle de niveau doctorat. Sujets : tribus (σ-algèbres), mesure de Lebesgue, fonctions mesurables, espaces Lp, convergence dominée. Notation automatique : principalement numérique (calculer une intégrale de Lebesgue, déterminer si une fonction est dans L^p) plus choix multiple sur le théorème de convergence applicable à un scénario donné — une correspondance quasi directe avec le programme de qualification en analyse réelle de Harvard [13].

9. Filière G3 — Analyse complexe. Sujets : holomorphie, théorème de Cauchy, résidus, applications conformes, théorème d’application de Riemann. Notation automatique : numérique (évaluer une intégrale de contour par les résidus — une tâche classique vérifiable par un système de calcul formel) plus choix multiple sur la classification des singularités.

10. Filière G4 — Topologie algébrique / Géométrie différentielle. Sujets : calcul d’homologie/cohomologie pour des espaces standards (sphères, tores, espaces projectifs), courbure de surfaces standards. Notation automatique : numérique (nombres de Betti, caractéristique d’Euler) — calculable et vérifiable — mais un contenu de démonstration véritable (par exemple, « démontre la dualité de Poincaré pour cet espace ») n’est pas évaluable automatiquement et devrait être présenté comme contenu d’« exemple travaillé » en lecture seule, pas comme un défi noté.

11. Filière Doctorat-1 — EDP et probabilités (socle des examens de qualification). Sujets : équations de la chaleur/des ondes/de Laplace, solutions faibles, bases des injections de Sobolev ; probabilités fondées sur la théorie de la mesure, fonctions caractéristiques, théorème central limite. Notation automatique : vérification numérique de solutions pour des EDP canoniques (vérifier qu’une solution candidate satisfait l’EDP et les conditions aux limites par substitution directe — purement mécanique et adapté au calcul formel) et questions de calcul de probabilités.

12. Filière Doctorat-Lean — Parcours de synthèse « formellement vérifié », clairement identifié comme distinct du reste. Sujets : une séquence organisée de petits lemmes (dans l’esprit du Natural Number Game) construisant vers un résultat non trivial, rédigés en Lean 4 contre mathlib. Notation automatique : le compilateur lui-même est le correcteur — une démonstration est notée réussite/échec par une compilation réussie, avec une ambiguïté de notation nulle, au prix d’un investissement de rédaction important (chaque exercice a besoin d’un squelette vérifiable par Lean) et d’un vrai coût de courbe d’apprentissage pour le joueur (la syntaxe Lean, pas seulement les mathématiques) [20][21].

13. Non-objectif explicite : la notation par IA de démonstrations libres en langage naturel comme mécanisme noté (pas comme rétroaction de tuteur). Étant donné le taux d’accord d’IMO-GradingBench, d’environ 52-54 % en notation aveugle avec des juges humains, même pour des modèles de pointe en 2025-2026 [22], Math Challenge ne devrait pas livrer de fonctionnalité qui attribue une note de réussite/échec ou une note chiffrée à des démonstrations en prose écrites par les étudiants sur le seul jugement d’un LLM. Il est en revanche approprié que la « rétroaction du tuteur IA après chaque défi » existante donne un commentaire qualitatif, non noté, sur une ébauche de démonstration soumise (c’est une fonctionnalité de coaching, pas une évaluation notée, donc un jugement erroné ou trop confiant est un problème de qualité d’expérience utilisateur, pas un problème d’intégrité de notation) — cette distinction (rétroaction contre note) est exactement ce qui garde les filières du mode Doctorat ci-dessus honnêtes sur ce que signifie « évaluable automatiquement ».

14. Mécanisme transversal : adopter l’idée clé de RefGrader — toujours noter par rapport à une référence, jamais en aveugle — pour tout jugement assisté par IA utilisé n’importe où dans le mode Doctorat. Puisque la notation agentique fondée sur une référence surpasse mesurablement la notation en aveugle [22][27], partout où le tuteur évalue un raisonnement ouvert (pas seulement le cas de non-objectif ci-dessus), il devrait toujours recevoir la solution canonique/la grille comme contexte, et ne jamais être invité à juger une démonstration à froid.

Questions ouvertes pour le propriétaire du projet

1. Le « mode Doctorat » devrait-il inclure le parcours de synthèse vérifié par Lean (point 12) compte tenu de son coût de rédaction, ou rester entièrement dans des formats numériques/choix multiple/contre-exemple ?
2. Une révision d’ébauche de démonstration par IA uniquement en coaching (non notée) est-elle acceptable pour les filières supérieures, ou le produit a-t-il besoin que chaque défi produise une note ferme de réussite/échec ?
3. Les limites des filières devraient-elles suivre strictement les codes principaux de la MSC (pour une fonctionnalité « parcourir par domaine MSC ») ou rester organisées autour du socle des examens de qualification du doctorat (plus restreint et plus standard sur le plan pédagogique) ?
4. Y a-t-il un intérêt pour licencier/intégrer un moteur existant adossé à un système de calcul formel (le pipeline Maxima de STACK est open source et natif de Moodle) plutôt que de construire la vérification d’équivalence numérique/symbolique à partir de zéro ?