Lors d’un entretien du World Science Festival le 2 octobre, le mathématicien Tristan Buckmaster a décrit un résultat produit avec l’IA qu’il juge correct, mais difficile à lire pour d’autres mathématiciens. Son récit précise la question soulevée par la récente annonce sur Navier–Stokes : comment une communauté de recherche peut-elle examiner un argument formel lorsqu’il faut encore travailler pour en donner une explication lisible ?

Buckmaster parlait de ses travaux avec Levent Alpöge sur les équations d’Euler tridimensionnelles avec une force régulière. Leur résultat est distinct de la revendication d’OpenAI du 8 septembre concernant les équations de Navier–Stokes avec une force régulière. Navier–Stokes inclut la viscosité ; Euler ne l’inclut pas. OpenAI a publié un article et une formalisation Lean pour son résultat revendiqué de perte de régularité en temps fini. L’institution qui administre le Millennium Prize n’a annoncé aucun prix.

Le grand changement

  • Ce qui a changé : Buckmaster a livré un témoignage de première main sur l’utilisation d’arguments générés par l’IA et de Lean pour établir le résultat distinct d’Euler forcé, ainsi que sur le travail encore nécessaire pour expliquer de telles preuves aux mathématiciens.
  • Pourquoi c’est important :Une vérification formelle peut établir qu’un argument encodé découle de définitions et de dépendances spécifiées. Les mathématiciens doivent aussi comprendre ce que dit le théorème, comment fonctionnent ses idées et à quels travaux antérieurs il fait appel.
  • À suivre :L’évaluation par Clay de la revendication d’OpenAI sur Navier–Stokes, des explications lisibles de la preuve et le débat public sur l’autorat et l’accès montreront comment ce résultat est évalué. La confiance de Buckmaster dans ce résultat est un avis d’expert, pas une décision d’attribution de prix.

Un argument vérifié a quand même besoin d’explications

Dans l’entretien, Buckmaster affirme que la première preuve de son résultat sur Euler produite par l’IA mêlait des idées utiles, des calculs sans pertinence et un texte difficile à lire. Son équipe a d’abord utilisé d’autres agents pour examiner chaque étape, puis a converti l’argument en Lean afin de le vérifier formellement. Il affirme que la preuve obtenue était correcte malgré sa présentation médiocre. Ce récit concerne ses travaux sur Euler; il ne faut pas y voir une vérification indépendante de chaque partie de l’autre article d’OpenAI sur Navier–Stokes.

La distinction est concrète. Lean vérifie un énoncé formalisé avec précision dans un environnement de preuve spécifié. Cela ne rend pas, à lui seul, un long argument lisible pour un chercheur qui voudrait réutiliser sa méthode. Buckmaster a dit à Brian Greene que d’autres systèmes d’IA pouvaient analyser des passages qu’il parvenait à peine à lire et que demander à l’IA de les traduire en langage mathématique courant était devenu une partie du travail. Il a également déclaré comprendre encore les idées de l’argument sur Navier–Stokes, même si le PDF publié était difficile à lire. Ce sont ses évaluations, pas un audit de preuve de BIG CHANGE ; nous n’avons pas exécuté les fichiers Lean ni arbitré l’un ou l’autre théorème.

Le compte rendu de NYU Courant du 14 septembre décrit le résultat de Buckmaster et Alpöge comme une perte de régularité en temps fini pour Euler forcé en 3D, avec une force régulière et des données initiales d’énergie finie. Il indique que trois articles de la collaboration ont été formalisés dans Lean et situe ce résultat dans une stratégie lancée par Diego Córdoba et Luis Martínez-Zoroa. Ces détails comptent pour l’attribution du mérite : une preuve produite par un modèle peut prolonger une voie mathématique existante sans effacer les personnes qui l’ont établie.

Deux résultats dans une séquence qui évolue rapidement

OpenAI dit que son système interne d’agents a d’abord produit un résultat pour les équations d’Euler sans force extérieure, puis a repris cette piste dans sa construction distincte sur Navier–Stokes. Son annonce reconnaît la priorité de Buckmaster et Alpöge pour le résultat d’Euler forcé, tout en affirmant que sa propre preuve a été développée indépendamment. Dans l’entretien, Buckmaster décrit les mécanismes mathématiques comme apparentés et dit qu’OpenAI a ajouté une idée de vortex en effondrement pour traiter la viscosité. Les récits s’accordent sur le fait que les revendications portent sur des équations et des étapes de preuve différentes ; ils ne règlent pas toutes les questions de chronologie ou de contribution intellectuelle.

La European Mathematical Society a salué l’annonce tout en soulignant les travaux antérieurs et en appelant à examiner l’autorat, la reconnaissance du mérite et l’accès au modèle interne. La réponse de Clay du 11 septembre indiquait que le problème de Navier–Stokes était apparemment résolu et que l’évaluation du résultat et l’attribution du mérite prendraient délibérément leur temps. Buckmaster a dit à Greene qu’il pense qu’OpenAI a une solution. Ces deux propos peuvent coexister : l’avis favorable d’un spécialiste et l’évaluation toujours en cours d’une institution.

Le récent retrait de trois autres manuscrits mathématiques d’OpenAI est un événement distinct. L’erreur de signe signalée justifie d’examiner chaque affirmation séparément ; elle ne prouve pas que la preuve de Navier–Stokes comporte la même erreur. Le guide de BIG CHANGE pour examiner un dépôt explique comment trouver les versions des manuscrits et les éléments de preuve, tandis que notre avis sur les capacités de relecture demande un soutien dédié à l’explication et à la vérification. L’article antérieur sur Navier–Stokes marque le début de cette séquence. L’entretien ajoute le témoignage d’un mathématicien en exercice sur ce qui suit la production d’un argument par un système d’IA.

Pour une affirmation aussi lourde de conséquences, les prochaines publications utiles seraient des comptes rendus précis et lisibles, des artefacts formels vérifiables et des réactions mathématiques indépendantes. Chacun remplit une fonction différente. La vitesse de génération d’une preuve candidate rend ces travaux plus urgents, tandis que la procédure annoncée par Clay laisse le temps de les mener soigneusement.

Sources et lectures complémentaires