OpenAI a déclaré le 26 octobre avoir publié une présentation en langage naturel et une formalisation Lean de ce qu’il décrit comme une preuve générée par IA de la conjecture de lissage local de Sogge de 1991 pour l’équation des ondes euclidienne.
Le dossier public se répartit entre l’annonce d’OpenAI et l’historique GitHub associé, qui décrivent la portée de manière légèrement différente. Le billet d’OpenAI affirme que le résultat prouve la conjecture dans toute dimension et résout donc la conjecture de Kakeya ainsi que la conjecture de restriction de Stein dans toutes les dimensions. La page d’historique GitHub est plus limitée : elle indique que le résultat couvre les ondes dans toute dimension spatiale d’au moins deux, entraîne les conjectures de maximal de Kakeya et de dimension, et fournit les estimations de restriction sphérique de Stein dans tout l’intérieur de l’intervalle conjecturé.
C’est important, car les artefacts de preuve sont publics et vérifiables, mais leur portée doit être lue à partir des deux sources plutôt que du seul billet de lancement.