Il y a des disciplines où l'irruption de l'intelligence artificielle se mesure en gains de productivité. Les mathématiques ne sont pas de celles-là. Ici, ce qui est en jeu touche au cœur du métier : la démonstration, cet enchaînement d'arguments dont la validité ne dépend ni d'une autorité ni d'un consensus, mais de la seule nécessité logique. Lorsqu'une machine produit un tel enchaînement, et que personne ne sait exactement comment elle y est parvenue, c'est le statut même du savoir mathématique qui vacille.
C'est ce basculement que décrit Le Monde, qui rapporte une « crise inédite » dans la communauté mathématique après l'annonce, par OpenAI, qu'un de ses modèles aurait résolu un problème majeur. Le quotidien français fait état de réactions oscillant entre la colère, l'inquiétude, la résignation et l'enthousiasme — un éventail émotionnel inhabituel pour un milieu qui, d'ordinaire, tranche ses querelles à coups de contre-exemples.
Une accélération de deux ans qui a tout bousculé
Pour comprendre la secousse, il faut revenir en arrière. En janvier 2024, la revue Nature publiait les travaux de Google DeepMind sur AlphaGeometry, un système capable de résoudre des problèmes de géométrie de niveau olympique sans démonstrations humaines en exemple. L'été suivant, DeepMind annonçait qu'un attelage de systèmes, AlphaProof et AlphaGeometry 2, atteignait un niveau équivalent à la médaille d'argent aux Olympiades internationales de mathématiques. La performance était spectaculaire, mais encore rassurante : les olympiades sont un exercice scolaire de haute voltige, pas de la recherche.
La suite a été plus rapide que prévu. Les modèles de langage généralistes, sans architecture dédiée à la géométrie ou à la logique formelle, se sont mis à grimper dans les classements. Les organismes d'évaluation ont dû fabriquer des épreuves plus dures : Epoch AI a ainsi conçu FrontierMath, un ensemble de problèmes inédits rédigés par des mathématiciens professionnels, précisément parce que les tests classiques étaient saturés. En moins de deux ans, la frontière est passée du concours étudiant à des questions que des chercheurs mettent des semaines à attaquer.
L'épisode qui a le plus marqué le milieu ne fut pourtant pas une démonstration, mais une confusion. À l'automne 2025, des employés d'OpenAI ont affirmé publiquement qu'un modèle avait « résolu » des problèmes ouverts issus de la célèbre liste de Paul Erdős. Il s'est avéré que le système avait surtout retrouvé dans la littérature des solutions déjà publiées mais mal indexées. Le mathématicien Thomas Bloom, gestionnaire du répertoire des problèmes d'Erdős, et Terence Tao, figure centrale de la discipline, ont dû corriger le tir. L'affaire a laissé une trace : elle a montré à la fois la puissance réelle de ces outils comme moteurs de recherche bibliographique surhumains, et la propension des laboratoires à sur-vendre leurs résultats.
Le vrai problème : qui vérifie?
D'où la question qui obsède aujourd'hui les spécialistes : que vaut une preuve que personne n'a le temps de relire? Une démonstration de recherche contemporaine peut faire des centaines de pages. Son arbitrage par les pairs prend des mois, parfois des années. Si une machine en produit dix par semaine, la communauté n'a tout simplement pas la capacité humaine de les valider.
Une partie de la réponse existait avant l'IA : les assistants de preuve. Lean, développé dans une communauté ouverte autour de sa bibliothèque mathlib, permet d'écrire une démonstration dans un langage formel que l'ordinateur vérifie ligne à ligne. Un résultat formalisé en Lean est certifié au sens le plus strict : ou il compile, ou il ne compile pas. Cette technologie, longtemps jugée trop laborieuse par la plupart des chercheurs, devient l'infrastructure de confiance indispensable. Elle explique aussi pourquoi les laboratoires d'IA s'y intéressent : un vérificateur automatique fournit un signal d'entraînement impitoyable, sans complaisance.
Mais la formalisation ne règle pas tout. Une preuve correcte n'est pas nécessairement une preuve éclairante. Les mathématiciens ne cherchent pas seulement à savoir si un énoncé est vrai; ils cherchent à comprendre pourquoi. Une sortie de machine de 40 000 lignes, validée par un compilateur et opaque à toute lecture humaine, coche la case de la vérité et rate celle de la compréhension. C'est exactement le débat qu'avait ouvert, en 1976, la démonstration assistée par ordinateur du théorème des quatre couleurs — sauf qu'à l'époque le phénomène restait isolé, et qu'il menace aujourd'hui de devenir la norme.
L'intuition, dernier bastion ou mythe confortable?
Le deuxième front du débat porte sur l'intuition. Beaucoup de chercheurs soutiennent que l'essentiel de leur travail ne consiste pas à démontrer, mais à choisir : repérer la bonne question, sentir qu'un objet mérite un nom, deviner qu'une analogie entre deux domaines éloignés cache une structure commune. Cette faculté de sélection, disent-ils, reste hors de portée de systèmes optimisés pour produire des réponses à des questions déjà posées.
D'autres, plus inquiets, font remarquer que l'argument a déjà servi — pour le jeu de go, pour le repliement des protéines — et qu'il n'a pas tenu. Ils observent surtout un effet de structure : si les modèles absorbent la partie technique du travail, celle qu'on confie traditionnellement aux doctorants et aux postdoctorants, c'est tout le mécanisme de formation d'un mathématicien qui se grippe. On n'acquiert pas d'intuition sans avoir sué sur des calculs ingrats. Une discipline qui externalise ses exercices risque de ne plus produire les cerveaux capables de superviser les machines.
Terence Tao, qui documente publiquement ses propres usages de ces outils, défend une voie intermédiaire : l'IA comme collaboratrice massive, permettant des projets collectifs jusqu'ici impensables, à condition que l'humain garde la main sur la formulation des problèmes et sur la formalisation des résultats. Son projet de classification d'équations algébriques, mené avec des dizaines de contributeurs et une vérification intégrale en Lean, préfigure ce mode de production hybride.
Un séisme scientifique dans un paysage industriel bruyant
Cette crise intellectuelle se déroule sur fond de bataille commerciale, et cela n'aide pas à y voir clair. Les annonces mathématiques sont devenues des arguments de vente dans une course où les laboratoires s'accusent mutuellement d'instrumentaliser les débats. RTE rapportait récemment que des entreprises européennes, Mistral en tête, reprochent à leurs rivales américaines d'invoquer la sécurité pour verrouiller leur avance — signe que chaque déclaration publique est aussi un coup stratégique.
Le contraste est d'ailleurs saisissant avec la diffusion réelle de ces technologies dans le monde du travail. Selon l'étude de l'Université de Constance relayée par Phys.org, la part des salariés utilisant l'IA dans leur quotidien professionnel n'est passée que de 35 % à 38 % en un an, avec des usages restés informels et très inégaux. Pendant que l'IA bouleverse les fondements d'une science vieille de vingt-cinq siècles, elle peine encore à s'installer dans les bureaux.
Pour les mathématiciens, la question n'est plus de savoir si les machines feront des mathématiques, mais quelle sorte de mathématiques survivra à leur présence. Une discipline de vérités certifiées et illisibles? Ou une discipline qui redéfinit sa valeur autour de ce que la formalisation ne capture pas : le sens, la hiérarchie des idées, le plaisir de comprendre. Le débat est ouvert, et il est, pour une fois, réellement indécidable.