Le 19 octobre, le journal étudiant The Daily Californian a publié des entretiens où deux mathématiciens de l’Université de Californie à Berkeley expriment des vues divergentes sur l’IA. En toile de fond, une analyse publiée le 6 octobre par A. Bastounis, F. Circelli et A. C. Hansen relève des écarts entre certains passages de la preuve écrite d’OpenAI sur Navier-Stokes et leur formalisation en Lean. Les auteurs ne concluent pas que la preuve en langage naturel est incorrecte.
Deux visions de l’IA en mathématiques
Richard Borcherds, professeur de mathématiques à Berkeley, estime que si les progrès actuels se poursuivent, l’IA pourrait rendre les chercheurs humains redondants dans quelques années. Robin Huang, doctorante en dernière année à Berkeley, se montre plus sceptique sur l’utilité actuelle de l’IA pour la recherche mathématique et s’inquiète de ses effets sur la communauté. Leurs propos reflètent des perspectives individuelles, pas un consensus des mathématiciens.
Ce qu’OpenAI affirme avoir démontré
Le 8 septembre, OpenAI a annoncé un résultat revendiqué sur les équations de Navier-Stokes incompressibles en trois dimensions. L’entreprise affirme qu’un fluide initialement au repos, soumis à une force extérieure régulière, peut développer une singularité en temps fini tout en conservant une énergie finie. Une singularité désigne ici un comportement où la solution cesse de rester régulière. OpenAI dit que son résultat répond aux assertions C et D de la formulation du problème du prix du millénaire.
OpenAI a aussi publié d’autres résultats mathématiques produits par un modèle interne, dans une publication distincte déjà présentée par NeoTeo.
Pour cette tentative sur Navier-Stokes, OpenAI a rapporté qu’environ 10 000 agents avaient travaillé simultanément, générant quelque 2,7 millions de messages et 130 milliards de tokens en sortie. L’entreprise a indiqué que les agents avaient produit le résultat en environ 88 heures, puis que la formalisation et la vérification en Lean avaient pris 17 heures supplémentaires.
L’écart relevé dans l’estimation
Lean est un assistant de preuve, un logiciel qui vérifie la validité logique d’une démonstration formalisée. Dans leur article du 6 octobre, A. Bastounis, F. Circelli et A. C. Hansen comparent notamment les versions d’une estimation du lemme 8.6 :
| Version de l’estimation | Dérivées supplémentaires dans la borne |
| Texte en langage naturel | 4 |
| Estimation citée en Lean | 5 |
Les auteurs relèvent aussi une différence dans une estimation du flux de pression : l’expression en langage naturel fait intervenir un terme en B_R, tandis que la version Lean dépend également de A_R. Ils indiquent que ces deux bornes sont difficiles à comparer.
Ce que la vérification en Lean permet de dire
Lean vérifie la preuve et l’énoncé tels qu’ils sont codés dans le système. Cela ne suffit pas à établir que cette formalisation correspond fidèlement au texte et au raisonnement en langage naturel. La critique de Bastounis, Circelli et Hansen porte sur cette correspondance dans les exemples qu’ils analysent, notamment l’estimation du lemme 8.6 et celle du flux de pression. Ils ne concluent pas que la preuve rédigée par OpenAI est incorrecte.
