L’essentiel
- OpenAI revendique une preuve d’effondrement pour les équations complètes de Navier-Stokes, l’un des sept problèmes du prix du millénaire.
- Environ 10 000 agents coordonnés ont abouti en 88 heures, suivies de 17 heures de formalisation et de vérification en Lean, pour plusieurs millions de dollars de calcul.
- Tristan Buckmaster (NYU) et Levent Alpöge (Anthropic) contestent l’attribution du résultat, après près d’un an de travail sur une version simplifiée du problème.
- Terence Tao alerte sur l’épuisement du stock de problèmes ouverts et sur la tentation, pour les chercheurs, de ne plus publier leurs pistes.
Samedi 5 septembre, un essaim d’environ 10 000 agents d’OpenAI a rendu une preuve d’effondrement pour les équations complètes de Navier-Stokes : la démonstration qu’un écoulement parfaitement régulier au départ peut voir sa vitesse devenir infinie en un temps fini. Ces équations décrivent le mouvement des fluides et résistent aux mathématiciens depuis près de deux siècles. Quatre-vingt-huit heures de calcul, puis dix-sept heures de formalisation en Lean, l’assistant de preuve qui vérifie mécaniquement chaque étape d’un raisonnement. L’annonce a occupé toute la journée de lundi. Le lendemain, Terence Tao publiait quelques lignes qui ont beaucoup moins circulé : les bons problèmes ouverts s’épuisent comme une ressource non renouvelable, et les chercheurs ont désormais intérêt à garder leurs pistes pour eux.
La machine accélère, la lecture humaine non
OpenAI a communiqué ses volumes : 4,9 millions de messages échangés entre agents et près de 300 milliards de tokens produits sur l’ensemble des problèmes attaqués, dont 2,7 millions de messages et environ 130 milliards de tokens pour le seul Navier-Stokes. Le modèle employé est interne, non publié, encore en cours d’entraînement, et présenté par l’entreprise comme nettement supérieur à GPT-6 Astra, sorti la semaine précédente. Google DeepMind travaille le même terrain par un autre chemin : son système AlphaProof Nexus, décrit en mai dans une prépublication arXiv, fait tourner des agents entre un modèle de pointe et le compilateur Lean, et a réglé 9 des 353 problèmes ouverts d’Erdős qui lui avaient été soumis.
La formalisation en Lean garantit qu’une démonstration ne comporte pas de trou logique. Elle ne dit rien de ce qui intéresse un mathématicien : la pertinence de l’approche, sa fécondité, ce qu’elle ouvre pour les problèmes voisins. Anthropic rappelait la semaine dernière qu’établir la validité d’une preuve majeure peut prendre des années. Produire une preuve demande désormais quatre jours ; la juger demande toujours autant d’années. Un goulot d’étranglement ne disparaît pas quand on accélère l’étape qui le précède, il se déplace.
Une rumeur a suffi à lancer l’essaim
La chronologie compte autant que le résultat. OpenAI situe le départ de son effort au 1er septembre, après avoir entendu qu’un problème du millénaire venait d’être résolu. Cette rumeur portait sur les travaux de Tristan Buckmaster, professeur à NYU, et de Levent Alpöge, mathématicien employé par Anthropic. Les deux hommes travaillaient depuis près d’un an, en s’appuyant sur Claude et sur Codex, et avaient obtenu leur percée le 15 août. Leur preuve, portant sur une version simplifiée des équations, a été publiée lundi sur Mastodon dans l’urgence.
Buckmaster raconte avoir demandé à quel moment le premier prompt avait été envoyé, et n’avoir obtenu la réponse qu’après insistance : dans les jours suivant l’arrivée de l’information chez OpenAI. Il dit avoir aussi demandé si le modèle avait été entraîné sur leurs sessions Codex, où ils déposaient tous leurs brouillons depuis un an. Sur l’accès aux données des utilisateurs, la réponse a été non, et Mark Chen a depuis démenti tout accès aux transcriptions. Sur l’entraînement, Buckmaster dit n’avoir jamais eu de réponse. On lui a proposé de cosigner l’article d’OpenAI, à condition d’en écarter Alpöge en raison de son employeur.
Rien dans ce dossier ne permet de trancher entre convergence indépendante et reprise implicite : les deux équipes partent d’une approche initiée par Diego Córdoba et Luis Martínez-Zoroa, et cette piste circulait dans la communauté. Une rumeur a pourtant suffi à déclencher une campagne de calcul de plusieurs millions de dollars sur un problème qu’une autre équipe tenait presque.
Un ticket d’entrée à plusieurs millions de dollars
Sébastien Bubeck et Mark Chen ont été explicites : l’équipe n’a abouti qu’en faisant tourner ces agents en parallèle, pour une facture de plusieurs millions de dollars. Javier Gómez-Serrano formule l’évidence que personne dans le milieu n’a envie de dire tout haut : très peu de mathématiciens disposeront un jour de telles ressources. Et nul ne sait quelles priorités de dépense retiendront les entreprises d’IA. Plusieurs chercheurs rapportent un climat déprimé dans la profession.
OpenAI annonce par ailleurs qu’elle ne réclamera pas le million de dollars attaché au problème depuis mai 2000. Geste élégant, et parfaitement rationnel : la démonstration de capacité vaut bien davantage pour l’entreprise que le prix Clay. L’épisode tient davantage de l’opération de calcul industriel que de la découverte de laboratoire, et cette asymétrie de moyens redéfinit qui a les épaules pour s’attaquer aux grandes questions.
Publier une piste devient un risque
Le stock de bons problèmes, ceux dont la résolution fait avancer un domaine entier, ne se reconstitue pas : c’est la mise en garde de Tao. Navier-Stokes lui donne un argument supplémentaire. La simple rumeur qu’une équipe travaille sur un sujet peut déclencher un effort massif qui l’aplatit avant que le projet initial ait donné tout ce qu’il contenait. D’où le réflexe qu’il redoute : taire ses directions prometteuses, dans une discipline dont les progrès reposent depuis des siècles sur la circulation des idées.
Le mécanisme dépasse les mathématiques. Un essaim capable de saturer un espace de recherche en quatre jours transforme toute piste rendue publique en cible. Les spécialistes situent d’ailleurs le point faible de ces modèles dans le « goût de recherche » : l’aptitude à choisir les bonnes questions, plutôt qu’à traiter en masse celles qu’on leur soumet. Ce goût-là se nourrit de ce que les humains publient. Si les carnets se ferment, l’essaim continuera de tourner, mais sur des problèmes de plus en plus pauvres.
Mon avis
Le résultat mathématique m’impressionne moins que la vitesse à laquelle une rumeur s’est transformée en opération industrielle contre une équipe de deux personnes. Je ne crois pas une seconde au scénario du secret généralisé décrit par Tao, parce que la carrière académique reste indexée sur la publication. Ce que je vois venir, ce sont des embargos privés et des collaborations sous accord de confidentialité entre labos et éditeurs d’IA, autrement dit une science ouverte de façade. Quand deux annonces concurrentes tomberont à quelques heures d’écart sur le même problème, plus personne n’aura le temps d’arbitrer qui a prouvé quoi.
