OpenAI a publié un ensemble de travaux portant sur les équations de Navier-Stokes, qui décrivent le comportement des fluides visqueux et figurent parmi les problèmes du prix du millénaire de l'institut Clay. Fait notable souligné par le blog technique de John D. Cook, cette publication inclut une preuve formelle rédigée dans Lean 4, un assistant de preuve de plus en plus utilisé par la communauté des mathématiciens pour vérifier rigoureusement des résultats complexes.
L'usage de Lean 4 dans ce contexte s'inscrit dans une tendance plus large: plutôt que de se contenter d'un raisonnement informel ou d'une démonstration produite par un modèle de langage, l'équipe a soumis le résultat à un vérificateur formel capable de contrôler chaque étape logique de façon mécanique. Cette approche répond à une préoccupation récurrente concernant les productions mathématiques des systèmes d'IA: leur tendance à produire des arguments plausibles mais erronés, difficiles à détecter sans une vérification indépendante.
Les détails précis sur la portée du résultat — s'agit-il d'un cas particulier, d'une construction de type explosion en temps fini, ou d'un résultat partiel sur l'existence et la régularité des solutions — restent à préciser dans la publication complète. Il ne s'agit pas, en l'état des informations disponibles, d'une résolution du problème du millénaire dans son ensemble, mais plutôt d'une contribution technique dont la validité formelle est garantie par construction grâce au vérificateur Lean.
Cette initiative confirme l'intérêt croissant d'OpenAI pour les mathématiques formelles, un domaine où l'entreprise investit depuis plusieurs années, notamment via des travaux sur la démonstration automatique de théorèmes. L'association entre génération par IA et vérification formelle en Lean pourrait devenir une pratique standard pour établir la crédibilité de résultats mathématiques produits ou assistés par des modèles de langage, en particulier lorsque ceux-ci touchent à des domaines aussi scrutés que les équations aux dérivées partielles.