Ce qui a réellement été démontré
Levent Alpöge et Tristan Buckmaster ont mis en ligne trois prépublications établissant une explosion en temps fini avec un terme de forçage régulier pour l’équation du milieu poreux incompressible, le système de Boussinesq bidimensionnel et les équations d’Euler incompressibles en trois dimensions.
Terence Tao a commenté ces résultats lundi, relevant que les arguments sont « fortement assistés par l’IA » et que le travail a également été formalisé en Lean. Il attribue le programme sous-jacent à Diego Córdoba et Luis Martínez-Zoroa, qui avaient traité les premiers le cas du milieu poreux.
L’explosion signifie que les équations produisent une solution dont la vitesse devient infinie en temps fini : une rupture mathématique, non physique. L’établir pour Euler avec forçage est une étape vers la même question pour Navier-Stokes, dotée d’un prix du millénaire de l’institut Clay.
La part de l’IA
Buckmaster est à l’université de New York. Alpöge est chercheur chez Anthropic. Selon Unite.AI, le duo a indiqué avoir utilisé Claude, d’Anthropic, et Codex, d’OpenAI, pour la tenue des ordres inductifs et des constantes, et pour affiner la rédaction par itérations.
Ils ont été directs sur la qualité de la prose produite par les modèles. Buckmaster a décrit le texte initial généré par l’IA comme « le plus horrible que j’aie jamais lu », et les auteurs ont qualifié leur premier jet de pire rédaction qu’ils aient vue. C’est la formalisation en Lean qui porte la certitude : un assistant de preuve accepte un argument ou ne l’accepte pas.
Le litige
Dans une déclaration publiée avec les prépublications, Buckmaster affirme qu’OpenAI lui a indiqué qu’un modèle interne avait produit une preuve d’environ 100 pages d’explosion en temps fini pour les équations de Navier-Stokes forcées. Il évoque deux conversations le 6 septembre avec des chercheurs d’OpenAI, dont Sébastien Bubeck.
Buckmaster écrit qu’OpenAI a proposé soit que les deux groupes publient à un jour d’intervalle, le résultat Navier-Stokes d’OpenAI suivant son article sur Euler, soit qu’il rédige seul le résultat Navier-Stokes en créditant un modèle interne non nommé d’OpenAI, Alpöge étant retiré de la liste des auteurs — un point que Buckmaster relie à l’emploi d’Alpöge chez Anthropic. Il rapporte s’être entendu demander, après son refus, pourquoi il ruinerait sa carrière. Il ajoute avoir demandé si les sessions Codex de son équipe avaient servi à l’entraînement et, selon ses mots, n’avoir pas obtenu de réponse.
Buckmaster reste prudent dans sa déclaration : il n’a pas vu la preuve d’OpenAI et écrit qu’il n’accuse personne de quoi que ce soit.
Bubeck a rejeté ce récit. OfficeChai a rapporté qu’il a qualifié ces affirmations de fausses et incendiaires, déclaré qu’OpenAI n’avait pas utilisé les prompts ni les preuves du duo pour solliciter ses propres modèles, et affirmé être entré dans la discussion en respectant les normes académiques. Il a indiqué qu’OpenAI était parvenu à Euler de façon indépendante par d’autres méthodes, et que son travail sur Navier-Stokes reposait sur une approche similaire, développée en un week-end.
Ce qui est tranché et ce qui ne l’est pas
Les résultats d’Alpöge et Buckmaster sont publics et vérifiés en Lean. L’annonce d’OpenAI sur Navier-Stokes ne l’est pas : lundi, l’entreprise n’avait pas publié le résultat sur sa propre page d’actualités, et aucun tiers n’a examiné la preuve.
Même si elle tient, la question du prix du millénaire n’est pas manifestement réglée. Scientific American a rapporté la réserve de Buckmaster lui-même : une partie de la communauté pourrait estimer que le problème n’a pas vraiment été résolu, puisque la version forcée repose sur un terme que la formulation classique exclut.
Ce qu’il faut surveiller est restreint et vérifiable : si OpenAI publie la preuve et son certificat Lean pour que d’autres la vérifient, et si l’institut Clay dit quelque chose des termes de forçage. Tant que le premier point n’est pas acquis, un camp de cette histoire a publié son travail et l’autre l’a décrit.
