Un mathématicien de l'université de New York et un chercheur d'Anthropic ont publié le 8 septembre une preuve d'explosion en temps fini pour les équations d'Euler incompressibles en trois dimensions sous forçage régulier, étendant un résultat antérieur obtenu sous des hypothèses plus grossières. Le travail a été mené avec l'aide de Claude et de Codex. Le point décisif : la preuve est vérifiée formellement.
Nous posions samedi la question de ce qu'est une preuve que personne ne peut vérifier. Voici la réponse, deux jours plus tard, et elle est meilleure que ce que nous espérions.
Ce que « vérifié formellement » signifie
C'est la différence entre cette annonce et celles que nous avons couvertes précédemment.
Quand un modèle produit une démonstration en langage naturel, on doit lui faire confiance ou la relire entièrement. Nous avons souligné à quel point cette confiance est mal placée, ces systèmes étant aussi assurés quand ils ont tort que quand ils ont raison.
Une preuve vérifiée formellement est écrite dans un langage que l'ordinateur peut contrôler ligne par ligne. Chaque étape doit se déduire mécaniquement des précédentes, selon des règles logiques explicites. Si une seule étape ne tient pas, le vérificateur refuse.
La conséquence est décisive : on n'a plus besoin de faire confiance au modèle. On a seulement besoin de faire confiance au vérificateur, qui est un programme relativement simple, écrit par des humains, audité par la communauté depuis des années.
Pourquoi c'est la bonne configuration
C'était exactement ce que nous appelions de nos voeux samedi, et il vaut la peine de le formuler clairement.
Le modèle fait ce qu'il fait bien : proposer. Explorer des pistes, suggérer des lemmes, essayer des constructions, produire du volume. C'est un travail où l'endurance compte, et où se tromper souvent n'a pas d'importance tant qu'on trouve parfois.
Le vérificateur fait ce que le modèle ne peut pas faire : garantir. Il ne comprend rien, il ne propose rien, il constate que chaque étape est valide.
Cette répartition résout le problème du double usage de la confiance. Elle transforme un résultat invérifiable en résultat vérifié, sans exiger qu'un humain lise l'ensemble.
Trois choses restent hors de portée du vérificateur, et il faut les nommer. Il valide que la preuve est correcte, pas qu'elle est intéressante : juger de l'importance d'un résultat reste humain. Il valide la démonstration, pas l'énoncé : si la question formalisée ne correspond pas à celle qu'on voulait poser, la preuve est juste et sans objet. Et il ne dit rien de la part respective de l'humain et de la machine dans la découverte, question que nous traitons ce soir dans un article séparé.
Pourquoi ce résultat précis compte
Sans entrer dans la technique, les équations dont il est question décrivent l'écoulement d'un fluide parfait. Savoir si leurs solutions peuvent devenir infinies en un temps fini — ce qu'on appelle une explosion — est un problème central de la physique mathématique, apparenté à l'une des grandes questions ouvertes du domaine.
Ce n'est donc pas un exercice de démonstration : c'est un sujet où des mathématiciens travaillent depuis des décennies, et où un résultat antérieur venait d'être obtenu sous des hypothèses moins satisfaisantes. Étendre ce résultat à un cadre plus régulier est un progrès réel.
Ce que ça dit de l'usage en recherche
Ce cas éclaire une distinction que nous avons posée dans notre article sur la capacité des modèles à avoir des idées.
Nous rapportions un test où les modèles échouaient largement à retrouver l'idée d'un article à partir de ses seules prémisses, avec des scores entre 3 et 15 %. Nous en concluions que ces systèmes excellent à exploiter le connu et butent sur ce qui ne l'est pas.
Ce travail ne contredit pas ce constat, il le précise. Le modèle n'a pas eu l'intuition à la place du chercheur : il a démultiplié sa capacité à explorer, tester et formaliser. C'est une collaboration où l'humain garde la direction et délègue l'endurance.
C'est probablement la configuration la plus productive, et elle est très différente de celle que suggèrent les communiqués annonçant qu'un modèle a résolu des problèmes ouverts.
Ce qu'il faut retenir
Ce résultat est important pour les mathématiciens et il l'est autant comme modèle méthodologique.
Il montre qu'on peut utiliser ces systèmes dans un cadre où leur principal défaut — produire du plausible avec assurance — est neutralisé par un dispositif extérieur. Ce n'est pas de la confiance, c'est de la vérification.
Nous écrivions samedi qu'une preuve que personne ne peut vérifier n'en est pas encore une, mais qu'elle peut le devenir si l'on peut vérifier ce qui la vérifie. C'est exactement ce qui vient d'être fait. La question qui reste est de savoir si cette exigence deviendra la norme, ou si l'on continuera d'annoncer des résultats sans elle parce que c'est plus rapide.