L’essentiel
- Timothy Gowers, médaille Fields, raconte sur son blog que GPT-5.6 Pro a résolu du premier coup, à deux reprises, des problèmes qu’il travaillait depuis longtemps.
- Des mathématiciens de Carnegie Mellon ont réglé un problème ouvert de théorie de Ramsey en avril 2026, en combinant solveurs SAT, code généré par des modèles de langage et vérification formelle.
- Abhishek Saha, professeur à Queen Mary University of London, estime que les modèles frontière valent déjà, dans son domaine, un doctorant solide et infatigable.
Deux fois, Timothy Gowers a soumis à GPT-5.6 Pro un problème sur lequel il avait passé un temps considérable. Deux fois, le modèle l’a résolu à la première tentative. Le médaillé Fields écrit sur son blog avoir éprouvé une sensation étrange, pas franchement agréable, comme si on lui tirait le tapis sous les pieds. Il se dit heureux, dans le même temps, que les problèmes soient enfin réglés.
L’âge d’or qu’il avait annoncé, et celui qui arrive
En 2000, le même Gowers décrivait une période faste à venir : les ordinateurs prendraient en charge les vérifications fastidieuses, les mathématiciens garderaient les idées. Les machines feraient toujours les parties ennuyeuses, écrivait-il, mais celles-ci seraient un peu moins ennuyeuses qu’avant. Il ajoutait dans la foulée que cet âge d’or, s’il advenait, avait peu de chances de durer : au cours du siècle suivant, les ordinateurs deviendraient assez bons pour démontrer des théorèmes et bouleverser la recherche en mathématiques pures.
Vingt-six ans plus tard, une équipe de mathématiciens de Carnegie Mellon estime que la période a commencé, et le dit en se réclamant explicitement de cette prédiction. Leur article d’avril 2026 règle un problème ouvert de théorie de Ramsey (la branche qui étudie l’ordre inévitable dans les grandes structures) en assemblant trois briques : un solveur SAT (un programme qui explore mécaniquement les combinaisons logiques jusqu’à trancher), du code produit par des modèles de langage, et une vérification formelle qui rend la preuve contrôlable ligne à ligne par une machine.
La promesse de 2000 reposait sur un partage net : le calcul à la machine, l’intuition à l’humain. Ce qui se produit ne respecte pas cette frontière. Gowers n’a pas perdu une vérification fastidieuse, il a perdu un problème qu’il avait choisi.
D’un côté un chef d’orchestre, de l’autre un chercheur dépossédé
Abhishek Saha décrit sur X une expérience opposée. Dans son domaine de recherche, les modèles frontière (les systèmes les plus avancés du marché) lui semblent aujourd’hui au moins aussi bons qu’un doctorant solide et infatigable. Il raconte une journée entière passée avec GPT-5.5 Pro sur du travail de routine qui lui aurait pris des semaines, et en tire une image : il joue de plus en plus le rôle du chef d’orchestre, au lieu de tenir tous les pupitres à la fois.
Deux chercheurs de haut niveau, la même génération d’outils, deux vécus incompatibles. Sur la puissance des modèles, pourtant, ils tombent d’accord. La divergence tient à ce que chacun a confié à la machine : Saha lui donne ce qu’il aurait délégué de toute façon, et récupère du temps ; Gowers lui a donné ce qu’il gardait pour lui, et récupère un résultat sans le chemin.
Quand produire ne coûte plus rien, vérifier devient le travail
Le prix qui s’effondre, c’est celui du temps de recherche : les mois de tâtonnement entre une idée et sa démonstration. L’intuition, elle, garde toute sa valeur. Elle change seulement de cible : le choix du problème.
L’épisode Erdős avait déjà donné le ton. Ce problème ouvert légué par le mathématicien hongrois est tombé face aux modèles ; une semaine plus tard, des chercheurs humains ont repris la technique de preuve pour l’adapter et réfuter une autre conjecture majeure (un énoncé tenu pour vrai mais jamais démontré). La machine a fourni le mécanisme, le transfert est resté humain. Depuis, les annonces s’enchaînent : Epoch AI, le groupe de recherche derrière le benchmark FrontierMath, a fait état d’une deuxième solution dans le volet de FrontierMath consacré aux problèmes ouverts, et OpenAI a présenté son modèle Astra en annonçant dix solutions de difficulté variable.
La solidité du résultat de Carnegie Mellon ne vient pourtant pas de la partie générative, mais de la vérification formelle, seule à garantir que la preuve tient. Google DeepMind pousse la même logique depuis AlphaProof, un système entraîné par renforcement qui rédige ses démonstrations en Lean (un langage de preuves vérifiables par ordinateur) et a atteint le niveau d’une médaille d’argent aux Olympiades internationales de mathématiques. La mécanique vaut bien au-delà des mathématiques : dès que la production devient quasi gratuite, la dépense se déplace vers le dispositif qui tranche si le résultat est bon, et vers la formulation de la question posée. Un modèle qui répond en trente secondes à une question mal posée ne fait pas gagner du temps. Il en fait perdre plus vite.
La scission que Saha voit venir
Saha s’attend à ce que sa discipline se coupe en deux. Certains s’adapteront vite et verront leur champ de travail s’élargir. D’autres resteront sceptiques jusqu’au bout, prévient-il, à la manière de John Henry, ce héros du folklore américain mort à la tâche en voulant battre une foreuse à vapeur. Le mathématicien Trefor Bazett, lui, table publiquement sur un nouvel âge d’or né de la rencontre entre l’ingéniosité humaine et les modèles.
Deux réserves, tout de même. Les benchmarks comme FrontierMath mesurent des problèmes à réponse vérifiable, ce qui ne recouvre qu’une fraction de l’activité réelle d’un chercheur, dont une bonne part consiste à décider ce qui vaut la peine d’être attaqué. Et un succès « du premier coup » ne dit rien du nombre de tentatives infructueuses ailleurs : personne ne publie les problèmes sur lesquels les modèles se cassent les dents.
Gowers avait annoncé que la fenêtre serait courte. Il l’écrivait comme une échéance, sans dramatiser. Son billet ajoute une chose que sa prédiction de 2000 ne contenait pas : le basculement se vit d’abord comme une contrariété très personnelle, longtemps avant de se lire dans une courbe.
Mon avis
Le malaise de Gowers m’apprend davantage que tous les scores publiés ce mois-ci : il mesure ce qu’aucun benchmark ne capte, la part d’identité qu’un chercheur avait placée dans le temps qu’il passait à chercher. Je crois que les mathématiques vont se réorganiser autour du choix des problèmes, et que la transition sera rude pour ceux dont la réputation reposait sur l’endurance technique. Et je n’exclus pas qu’on regarde bientôt cette période avec nostalgie : le jour où les modèles passeront du théorème isolé à la question à poser, il ne restera plus de refuge confortable en amont.
