Physical Superintelligence (PSI) a annoncé le 6 novembre 2026 qu'un système interne de recherche IA, tournant sur des instances d'un modèle Anthropic non public, avait trouvé une preuve de la conjecture d'Aaronson-Ambainis, une question d'informatique quantique ouverte depuis 2008. Le système a produit une preuve complète au troisième jour d'une exécution sur l'infrastructure propre de PSI, et Lean — un assistant de preuve qui vérifie par machine chaque étape d'un raisonnement mathématique — l'a acceptée. PSI a ensuite lancé le système sur des problèmes ouverts voisins, amélioré le résultat à deux reprises, et Lean a accepté la version finale. Le manuscrit et la formalisation en Lean 4 sont publics.

La conjecture demande quand les ordinateurs quantiques peuvent être exponentiellement plus rapides que les machines classiques. Si la preuve de PSI tient, un ordinateur ordinaire peut estimer la probabilité qu'un algorithme quantique réponde oui, pour la plupart des entrées et avec une marge d'erreur fixe, sans lire l'entrée exponentiellement plus de fois — autrement dit, les accélérations quantiques exponentielles exigent des motifs ou une structure particuliers dans le problème, une limite longtemps soupçonnée mais jamais prouvée. PSI indique que sa preuve suit un plan tracé par Shachar Lovett et Jiapeng Zhang, qui avaient laissé une inégalité clé non prouvée ; le nouvel article prouve une inégalité de remplacement et donne une borne explicite.

Ce qui rend cette annonce plus difficile à écarter qu'un titre habituel du type « l'IA a résolu les maths », c'est la vérification. Le dépôt de PSI indique que le développement formel ne contient ni espaces réservés pour des preuves ni axiomes ajoutés, et que ses déclarations ont été rejouées via le noyau de Lean et lean4lean, une implémentation indépendante du vérificateur de types de Lean. Dans une exécution en bac à sable, un comparateur utilisant les noyaux nanoda et Lean a accepté les quatre théorèmes finaux, et sur une deuxième machine, il a accepté une petite solution correcte et rejeté quatre solutions délibérément fausses. David Turturean, membre de l'équipe technique de PSI, a construit le système de recherche, cadré le problème, demandé au modèle de préparer un premier jet, relu ce jet et répond de l'exactitude de l'article ; Jim Halverson, conseiller de PSI, a audité la preuve, et le dépôt précise que des modèles d'IA ont produit les énoncés mathématiques, le premier jet et la formalisation Lean.

Les réserves sont réelles, et PSI les énonce lui-même. Le résultat n'est pas évalué par les pairs : la preuve n'a pas encore passé l'examen d'une revue, et des experts humains doivent encore confirmer que l'énoncé formel encodé en Lean correspond bien à la conjecture telle qu'Aaronson et Ambainis l'entendaient — l'article lisible par un humain n'est pas lui-même vérifié par machine. Quatre chercheurs de Stanford, qui ont réglé un cas particulier en août 2026, lisent la preuve et en rédigent une version plus courte pour les experts. Il faut donc voir cela comme une annonce d'entreprise assortie d'un artefact vérifiable, pas comme un verdict de revue — mais c'est une annonce frappante : elle suit la publication par OpenAI, en octobre, de 722 manuscrits mathématiques rédigés par IA, et c'est la preuve la plus solide à ce jour que les systèmes d'IA passent de l'assistance aux preuves à leur production.

Sources