Le dernier modèle d'inférence interne d'OpenAI a annoncé dix avancées mathématiques impressionnantes d'un seul coup.
Cela inclut :
- A démontré pour la première fois l'existence de groupes non sofiques ;
- A présenté de nouvelles bornes inférieures de circuit (Circuit lower bounds) ;
- A résolu la limite de difficulté du problème du vecteur le plus proche (Closest Vector Problem, CVP) ;
- Et le théorème de répétition parallèle à décroissance exponentielle pour les jeux quantiques à deux joueurs (Quantum parallel repetition).
Ce qui préoccupe le plus le professeur adjoint Henry Yuen de l'Université Columbia, c'est le dernier —
En 2016, Yuen a fait des progrès majeurs sur cette question, mais ne l'a pas résolue complètement. Pendant 10 ans, il a échoué à plusieurs reprises, et même il y a un mois, il a encore tenté de conquérir la preuve ultime avec ChatGPT 5.5, sans grand succès.
Et l'IA, sur son épaule, a donné un léger coup de pied pour envoyer le ballon dans le but.
La preuve est juste, mais les humains n'ont pas compris.
Il y a quelques jours, Lijie Chen a envoyé une ébauche de l'article à Henry Yuen et à quelques autres personnes.
À l'époque, sa vie était bien remplie et il n'avait pas le temps de lire en profondeur. Maintenant, l'article a été publié. Il ne peut plus se retenir et a quelque chose à dire.
Le théorème de la répétition parallèle quantique est le domaine sur lequel Henry Yuen a travaillé pendant plusieurs années pendant ses études supérieures, et qu'il considère comme son achievement le plus fier.
Henry Yuen, actuel professeur adjoint en sciences informatiques à la famille Srivani à l'Université Columbia
Il se souvient des après-midi passés dans les cafés, des nuits passées assis à son bureau, et des innombrables week-ends qu'il aurait dû passer à se reposer, à décomposer et à étudier à plusieurs reprises 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, ce qui le tenait éveillé la nuit, tourmenté. Il a ingurgité des tonnes d'outils mathématiques et a finalement réussi à démontrer la décroissance polynomiale.
https://arxiv.org/pdf/1604.04340
Plus important encore, il a acquis confiance en lui, a enfin reconnu ses propres capacités et a prouvé qu’il était effectivement capable de résoudre certains problèmes (du moins une partie) qui préoccupent également les autres.
Il croit que la preuve d'OpenAI devrait être correcte, étant donné qu'une preuve formalisée en Lean existe déjà. Toutefois, Henry Yuen aura besoin de quelque temps pour assimiler cette nouvelle preuve.
Bien que la nouvelle preuve reprenne effectivement où il avait cessé, l'IA a dépassé les limites de sa stratégie de preuve originale en utilisant certaines techniques et méthodes qui pourraient déjà être connues des chercheurs en théorie des opérateurs et en analyse fonctionnelle.
Outre l'excitation, la première réaction de Yuen a été la déception, concernant le style d'écriture de l'article.
Il a dit que ce certificat semblait fortement écrit par une IA : des introductions longues et tournantes, avec des éléments clés qui apparaissent comme par magie, laissant le lecteur perplexe.
La preuve d'OpenAI est intéressante à lire, mais aussi un peu frustrante.
Il pose d'abord le problème de manière claire, puis saute brusquement vers l'idée de « trouver la bonne purification à l'aide d'une pré-solution », sans laisser presque aucune étape logique entre les deux.
Ensuite, une série de calculs de l'entropie de matrice assez atypiques, compliqués et tortueux, vous concluent finalement : ce chemin est praticable.
Mais il ne précise pas d'où vient cette étape la plus cruciale, cet instinct.
Et la touche la plus subtile, la plus exigeante en créativité — la technique d'expansion de l'espace des opérateurs à l'aide de la transformation d'Uhlmann — qui aurait dû constituer le point culminant le plus émouvant de la démonstration, a été abandonnée par l'IA comme du sable, sans avertissement ni explication, rejetée à la section quatre.
La preuve correcte, mais l'idée la plus importante est cachée.
Il souhaite qu'OpenAI utilise plusieurs prompts pour bien réorganiser ce manuscrit.
Ce qui est encore plus douloureux, c’est le deuxième niveau : passer la vérification de Lean ne signifie pas comprendre.
La machine peut garantir que chaque étape de déduction est inattaquable, mais elle ne peut pas répondre à ces questions : « Pourquoi cette méthode fonctionne-t-elle ? », « Que signifie-t-elle dans le cadre plus vaste de la théorie ? », « Où d’autre peut-elle être utilisée ? » — Lean ne répond à aucune d’entre elles.
Yuen a reconnu qu'il est encore en train de digérer cette preuve.
La réponse est devant lui, mais il doit, comme s'il lisait un article d'amateur, reconstituer ligne par ligne l'intuition que l'IA n'a pas exprimée.
Oui, il y a bien une preuve de Lean là-bas. Mais ce n’est qu’une formalisation, cela ne signifie pas que je l’ai compris. Pour vraiment l’intégrer, il faudra probablement du temps et de la pratique.
En effet, l'IA élargit les frontières de la compréhension humaine, mais ensuite ? Quelle reste la joie et le sens de la recherche ? S'il résout tous les problèmes qui le hantent, qu'est-ce qui lui reste ?
Les questions se succèdent. Mais un point devenait de plus en plus clair pour lui : les jours à venir du mathématicien ne seraient pas tranquilles ; il devrait dompter ces géants de la pensée et traduire leur jargon en langage clair.
L'IA « réfute » une conjecture mathématique centenaire : une mise au point ! Lean n'est pas une boîte sécurisée
La semaine dernière, Ramana Kumar a infirmé la célèbre conjecture mathématique non résolue, la conjecture de Collatz, en 300 lignes de Lean.
La question est très simple : étant donné un entier positif, appliquez répétitivement deux règles — si le nombre est pair, divisez-le par 2 ; s’il est impair, multipliez-le par 3 et ajoutez 1 — finira-t-il toujours par atteindre 1, quel que soit le nombre de départ ?
Vous pouvez calculer :
This conjecture states that no matter which positive integer you start with, you will eventually fall into the 4→2→1 cycle.
Depuis que le mathématicien Lothar Collatz l'a posée en 1937, personne n'a pu démontrer sa validité ni trouver de contre-exemple.
Il a été qualifié par le mathématicien Paul Erdős : « Les mathématiques ne sont pas encore prêtes pour de tels problèmes », et par Jeffrey Lagarias, membre de l'Académie nationale des sciences des États-Unis et mathématicien, qui estime que « c'est un problème extrêmement difficile, totalement au-delà des capacités des mathématiques actuelles ».
If falsified, it would undoubtedly be a groundbreaking news in the mathematical community.
Malheureusement, trois jours plus tard, cette preuve formelle en Lean a été déclarée invalide, car elle exploitait en réalité une faille sous-jacente du noyau de Lean.
Daniel Selsam d'OpenAI, accompagné d'une IA spécialisée en cybersécurité, a aidé Lean FRO à effectuer une audit du noyau.
Ils ont découvert plus d'une vulnérabilité dans le noyau Lean !
Presque en même temps, le professeur de mathématiques à l'université Rutgers et conseiller de l'organisation de recherche Lean, Alex Kontorovich, a publié un message pour avertir : ne considérez pas Lean comme un vérificateur universel.
Il a directement ciblé le point faible : l'alignement sémantique (Semantic Alignment).
Même si le noyau Lean est infaillible, Lean ne s'occupe que de la compilation du code. Qui garantit que les « définitions » que vous écrivez dans le code correspondent bien à l'« intention intuitive » humaine exprimée en langage naturel ?
Ce que Lean peut confirmer, c'est une seule chose : le code compile et la logique formelle est correcte. Mais il ne vérifie absolument pas une question encore plus cruciale : cette déclaration formelle correspond-elle vraiment au théorème que vous souhaitez démontrer ?
La preuve est correcte, mais l'énoncé a été copié错误, Lean continue de donner le feu vert.
Ce problème d'alignement ne peut pas être résolu uniquement par ordinateur.
Lors de la conférence ICM 2026, Kontorovich a souligné que le plus grand aveuglement des mathématiques formalisées ne réside pas dans « la bonne dérivation », mais dans « le bon énoncé ». La dernière vérification doit encore être effectuée par des experts humains.
L'expérience Liquid Tensor a atteint le statut de légende précisément grâce à un examen manuel quasi obsessionnel de chaque définition mathématique par les chercheurs.
En combinant les propos des deux professeurs, on arrive à la même conclusion : l’IA peut prouver, les machines peuvent vérifier, mais la compréhension et la supervision restent du ressort de l’être humain.
Enfin, une rumeur sur les modèles d'inférence 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 WeChat « Nouvelle Intelligence », auteur : Apocalypses de l'ASI ; éditeur : David