OpenAI affirme avoir résolu un problème à un million de dollars avec 10 000 agents IA

OpenAI affirme avoir trouvé un contre-exemple à la régularité de certaines solutions tridimensionnelles des équations de Navier–Stokes : un fluide initialement lisse pourrait développer une singularité en temps fini. Le laboratoire rend publics un texte de preuve et une version formalisée dans Lean, un langage qui permet de vérifier les étapes logiques. Rendre une preuve mécaniquement vérifiable plutôt que de demander qu’on la croie sur parole : c’est la bonne méthode, et elle devrait devenir la norme.

La discipline va devoir lire plus vite qu’elle n’en a l’habitude

La formalisation est une pièce solide, mais l’annonce reste celle d’OpenAI : la portée du résultat, ses hypothèses et sa place dans le problème du millénaire devront être évaluées par des spécialistes indépendants, et l’entreprise dit ne pas demander le prix associé. L’objection qu’on entend déjà, « ce n’est pas une vraie preuve tant que la communauté n’a pas tranché », vaut pour tous les résultats mathématiques depuis toujours. La nouveauté n’est pas la prudence exigée, elle est le délai : une machine produit désormais en semaines ce qu’un domaine met des années à valider. C’est la validation qu’il faut accélérer, pas la production qu’il faut brider.

Cette architecture ressemble moins à une réponse instantanée qu’à un laboratoire de recherche automatisé : pistes parallèles, échanges, consolidation, puis vérification. Elle déplace la question centrale de l’IA scientifique. Demander encore si un modèle « sait raisonner » n’a plus grand intérêt ; ce qui compte est de savoir comment ses recherches sont pilotées, auditées et reproduites. Les institutions capables de répondre à celle-là prendront dix ans d’avance sur celles qui débattent encore de la première.