Le dernier modèle de raisonnement interne d’OpenAI a publié dix avancées mathématiques stupéfiantes d’un seul coup.
Parmi elles :
- La première preuve de l’existence de groupes non-sofiques (Non-sofic groups) ;
- De nouvelles bornes inférieures de circuits (Circuit lower bounds) ;
- La résolution de la limite de difficulté du problème du vecteur le plus proche (Closest Vector Problem, CVP) ;
- Ainsi que le théorème de décroissance exponentielle pour la répétition parallèle de jeux quantiques à deux joueurs (Quantum parallel repetition).
Ce qui intéresse le plus Henry Yuen, professeur associé à l’Université Columbia, c’est le dernier point —
En 2016, Yuen avait réalisé des progrès significatifs sur ce problème sans le résoudre complètement. Pendant 10 ans, il a échoué à plusieurs reprises. Il y a un mois, il utilisait encore ChatGPT 5.5 pour repartir à l’assaut de la preuve ultime, mais avec peu de résultats.
Et l’IA, sur ses épaules, a simplement poussé le ballon dans le but.
La preuve est correcte, mais l’humain ne la comprend pas
Il y a quelques jours, Lijie Chen a envoyé à Henry Yuen et à quelques autres un projet d’article.
Il était très occupé à l’époque et n’a pas eu le temps de l’étudier en profondeur. Maintenant, l’article est publié. Il a quelque chose à dire.
Le théorème de répétition parallèle quantique (Quantum parallel repetition theorem) est un domaine auquel Henry Yuen a consacré des années de dur labeur pendant ses études supérieures, et dont il est le plus fier.
Henry Yuen, professeur associé en informatique (famille Srivani) à l’Université Columbia
Il se souvient de ces après-midi passés dans les cafés, des nuits blanches au bureau, et de tous ces week-ends où il aurait dû se reposer, à démonter et étudier le théorème classique de répétition parallèle de Ran Raz.
Il voulait résoudre la version quantique de ce théorème, au point de ne pas pouvoir dormir et de se tourner et se retourner dans son lit. Il a ingurgité des tonnes d’outils mathématiques et a finalement réussi à prouver la décroissance polynomiale.
https://arxiv.org/pdf/1604.04340
Plus important encore, il y a puisé la confiance nécessaire pour enfin reconnaître ses propres capacités et prouver qu’il pouvait réellement résoudre des problèmes (au moins en partie) qui importaient aussi aux autres.
Il pense que cette preuve d’OpenAI est probablement correcte, étant donné qu’il existe déjà une preuve formalisée en Lean. Mais pour digérer cette nouvelle preuve, Henry Yuen a besoin d’un peu de temps.
Bien que la nouvelle preuve parte effectivement de l’endroit où il avait arrêté, l’IA a contourné les limites de sa stratégie de preuve initiale en utilisant quelques astuces et méthodes. Ces méthodes étaient peut-être déjà maîtrisées par les chercheurs en théorie des opérateurs (operator theory) et en analyse fonctionnelle (functional analysis).
Au-delà de l’excitation, le premier sentiment de Yuen fut la déception, une déception liée au style rédactionnel de l’article.
Il dit que cette preuve a une odeur d’IA : des préambules interminables qui tournent en rond, et des étapes clés qui apparaissent comme par magie, laissant le lecteur perplexe.
La preuve d’OpenAI est intéressante à lire, mais aussi un peu frustrante.
Elle commence par poser le problème bien droit sur la table, puis fait soudainement un bond vers la direction « utiliser la résolvante pour trouver la bonne purification », avec presque aucune marche logique intermédiaire.
Ensuite, s’ensuit une série de calculs d’entropie matricielle assez inhabituels, qui tournent et virent, pour finalement annoncer : cette voie fonctionne.
Mais l’étape la plus cruciale, l’intuition d’où elle vient, n’est pas expliquée.
Et la touche la plus ingénieuse, la plus créative — l’astuce de la dilatation de l’espace des opérateurs via la transformation d’Uhlmann (Uhlmann transformation), qui devrait être le point culminant le plus passionnant de toute la preuve, est jetée par l’IA comme un caillou, sans avertissement ni explication, dans la section 4.
Une preuve correcte, qui cache l’idée la plus importante.
Il souhaite qu’OpenAI consacre quelques invites de plus pour bien structurer ce manuscrit.
Le second point est encore plus douloureux : Le fait que Lean valide ne signifie pas la compréhension.
La machine peut garantir que chaque déduction est impeccable, mais les questions « pourquoi cette astuce fonctionne-t-elle », « ce que cela signifie dans le paysage théorique plus large », « où ailleurs peut-on l’appliquer » — Lean ne peut répondre à aucune de ces questions.
Yuen admet qu’il est encore en train de digérer cette preuve.
La réponse est là, sous ses yeux, mais il doit, comme s’il lisait un article d’un non-initié, reconstruire ligne par ligne l’intuition que l’IA n’a pas exprimée.
Certes, il y a une preuve Lean là-bas. Mais ce n’est qu’une formalisation, cela ne signifie pas que j’ai compris. Pour vraiment la digérer, il faudra probablement du temps et de la patience.
En effet, l’IA élargit les frontières de la compréhension humaine, mais ensuite ? Que reste-t-il du plaisir et du sens de la recherche ? Si l’IA résout tous les problèmes qui le hantent, que lui reste-t-il ?
Les questions s’enchaînent. Mais une chose dont il est de plus en plus certain : les mathématiciens ne vont pas s’ennuyer dans les temps à venir. Ils devront à la fois apprivoiser ces géants de la pensée et traduire leur jargon en langage humain.
La « réfutation » par l’IA d’une conjecture mathématique séculaire s’avère fausse ! Lean n’est pas non plus une boîte de sûreté
La semaine dernière, Ramana Kumar a utilisé 300 lignes de Lean pour réfuter la conjecture de Collatz (Collatz conjecture), l’un des problèmes mathématiques non résolus les plus célèbres.
La question qu’elle pose est très simple : prenez un entier positif, appliquez deux règles de manière répétée — divisez par 2 si le nombre est pair, multipliez par 3 et ajoutez 1 s’il est impair — finirez-vous toujours par tomber sur 1, peu importe le nombre de départ ?
Vous pouvez essayer :
Cette conjecture affirme que : quel que soit l’entier positif avec lequel vous commencez, vous finirez par tomber dans ce cycle 4→2→1.
Depuis que le mathématicien Lothar Collatz l’a proposée en 1937, personne n’a pu prouver qu’elle est vraie, ni trouver de contre-exemple.
Le mathématicien Paul Erdős l’a qualifiée de : « Les mathématiques ne sont pas encore prêtes pour de tels problèmes », et Jeffrey Lagarias, membre de l’Académie nationale des sciences des États-Unis et mathématicien, estime que « c’est un problème exceptionnellement difficile, complètement hors de portée des mathématiques actuelles ».
Si elle était réfutée, ce serait une nouvelle explosive pour les mathématiques.
Malheureusement, trois jours plus tard, cette preuve formalisée en Lean a été jugée invalide car elle exploitait en réalité une vulnérabilité de bas niveau du noyau de Lean.
Daniel Selsam d’OpenAI, avec une IA spécialisée en cybersécurité, a aidé Lean FRO à réaliser un audit du noyau.
Résultat : ils ont découvert non pas une, mais plusieurs vulnérabilités dans le noyau de Lean !
Presque au même moment, Alex Kontorovich, professeur de mathématiques à l’Université Rutgers et conseiller pour un groupe de recherche spécialisé sur Lean, a posté un message pour avertir : ne considérez pas Lean comme un vérificateur universel.
Il pointe directement le talon d’Achille — l’alignement sémantique (Semantic Alignment).
Même si le noyau de Lean est irréprochable, Lean ne fait que compiler le code. Qui garantit que la « définition » que vous écrivez dans le code correspond bien à « l’intention intuitive » que les humains ont dans le langage naturel ?
Lean ne peut confirmer qu’une chose : le code compile, la logique formelle est correcte. Mais il ne vérifie absolument pas une question bien plus cruciale : Cet énoncé formalisé correspond-il vraiment au théorème que vous voulez prouver ?
Si le théorème est prouvé correctement mais que l’énoncé du problème est mal recopié, Lean donnera quand même son feu vert.
Et ce problème d’alignement ne peut pas être résolu uniquement par ordinateur.
Dans son discours à l’ICM 2026, Kontorovich l’a souligné : le plus grand angle mort des mathématiques formalisées n’est pas dans « avoir raisonné correctement », mais dans « avoir dit la bonne chose ». Les derniers garde-fous doivent être des experts humains.
La raison pour laquelle l’expérience Liquid Tensor (Liquid Tensor Experiment) est devenue légendaire tient précisément à l’examen humain quasi-obsessionnel de chaque définition mathématique par les chercheurs.
En rapprochant les propos des deux professeurs, ils pointent vers le même fait : l’IA peut prouver, la machine peut vérifier, mais la compréhension et le contrôle final restent le travail des humains.
Enfin, une petite anecdote sur les modèles de raisonnement par IA :
Références :
https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/
https://x.com/AlexKontorovich/status/2083919186825236831
https://x.com/henryquantum/status/2083623700608237956
Cet article provient du compte officiel WeChat « 新智元 » (New Wisdom Era) ; auteur : ASI Apocalypse ; éditeur : David
