Dans un article publié le 13 octobre 2026, Scientific American rapporte que plusieurs groupes d’experts jugent de plus en plus que la méthode du grand essaim final d’OpenAI diffère du programme associé aux mathématiciens Diego Córdoba et Luis Martínez-Zoroa. Une analyse technique distincte relève, elle, un écart entre un énoncé de l’article d’OpenAI et l’estimation correspondante en Lean : deux questions à ne pas confondre. Scientific American

Les experts distinguent la méthode de l’essaim final

Selon Scientific American, les deux démarches partagent une stratégie générale : construire une force artificielle, admise par la formulation du problème de Clay, pour obtenir le comportement recherché. Mais la force est construite différemment dans l’approche du grand essaim final. Certains experts estiment qu’un groupe préliminaire plus restreint a pu suivre le programme espagnol pour obtenir un résultat intermédiaire. L’influence éventuelle de ce programme sur le raisonnement du système reste indéterminée, indique le compte rendu. Scientific American

Lean vérifie un énoncé formel ; sa fidélité au texte est une autre question

Lean est un assistant de preuve : il vérifie une démonstration par rapport à un énoncé formel encodé. Cette vérification ne garantit pas, à elle seule, que l’énoncé encodé correspond fidèlement à celui de l’article rédigé en langage naturel. C’est cette correspondance que discutent A. Bastounis, F. Circelli et A. C. Hansen dans leur analyse des résultats formalisés par OpenAI. Analyse de Bastounis, Circelli et Hansen

Le lemme 8.6 : quatre dérivées dans le texte et cinq dans Lean

Dans cette vidéo en anglais, Adem B10 explique l’écart de dérivées entre le lemme 8.6 écrit et l’estimation Lean.

Pour le lemme 8.6, les auteurs comparent une borne qui demande quatre dérivées supplémentaires de la donnée d’entrée dans l’article à une estimation Lean qui en utilise cinq. L’écart concerne cette estimation intermédiaire : les auteurs ne concluent pas que la preuve d’OpenAI rédigée en langage naturel est fausse. Ils relèvent aussi une différence entre les formulations de l’estimation du flux de pression de l’équation 10.19 et jugent ces formes difficiles à comparer directement. Analyse de Bastounis, Circelli et Hansen

Version examinéeDérivées supplémentaires de la donnée d’entréePassage
Article en langage naturel4Lemme 8.6, équation (8.19)
Estimation Lean examinée5Lemme 8.6

La portée de la revendication d’OpenAI

Dans son annonce du 8 septembre 2026, OpenAI affirme que sa construction part d’un fluide incompressible à trois dimensions, initialement au repos et régulier, soumis à une force extérieure régulière. Selon l’entreprise, ce fluide peut développer une singularité en temps fini tout en conservant une énergie finie ; OpenAI dit établir les énoncés C et D de la formulation du problème par le Clay Mathematics Institute. Annonce d’OpenAI Formulation du problème par le Clay Mathematics Institute