Physical Superintelligence (PSI), une startup de recherche en physique, a affirmé qu'un modèle d'IA d'Anthropic, encore non public, a aidé à démontrer la conjecture d'Aaronson-Ambainis, un problème de calcul quantique ouvert depuis 2008. L'annonce a été faite le 6 novembre et indique qu'un programme a vérifié la preuve étape par étape.
La conjecture, formulée par les scientifiques Scott Aaronson et Andris Ambainis, porte sur les conditions dans lesquelles un ordinateur quantique peut être exponentiellement plus rapide qu'un ordinateur classique. La question concerne les données aléatoires, qui n'ont presque jamais le motif caché que ces machines exploitent. Si la conjecture est vraie, dans ces cas, l'avantage quantique n'est jamais exponentiel.
Selon PSI, la preuve est issue d'un système de recherche créé au sein de l'entreprise et exécuté sur son propre infrastructure. Ils y ont exécuté des « instances d'un modèle non public d'Anthropic », que l'entreprise n'identifie pas. Le système a obtenu la démonstration complète au cours du troisième jour d'exécution, selon le texte de PSI.
Le programme qui l'a acceptée s'appelle Lean, un assistant de démonstration qui vérifie chaque étape d'un raisonnement mathématique. PSI indique qu'il a ensuite fait travailler le système sur des problèmes connexes et qu'il a amélioré le résultat à deux reprises, et que Lean a accepté la version finale.
Qu'est-ce qui est vérifié et qu'est-ce qui ne l'est pas
L'entreprise a publié sur GitHub l'article et le code de la vérification. Selon le fichier explicatif du dépôt, les quatre théorèmes finaux ont été vérifiés sans lacunes ni hypothèses ajoutées, et deux implémentations indépendantes de Lean ont répété le contrôle. N'importe qui peut exécuter ces tests.
Le même document reconnaît des limites. Il revient à un lecteur humain de confirmer que l'énoncé écrit en Lean équivaut à la conjecture telle qu'elle a été publiée par Aaronson et Ambainis. L'article lui-même n'a pas été vérifié par une machine, et l'un des théorèmes dépend d'un résultat d'autres auteurs qui n'a pas été formalisé.
Il n'y a pas non plus de révision par les pairs, le contrôle par d'autres spécialistes que les revues scientifiques exigent. L'analyse d'explainx.ai, un blog sur l'IA, indique qu'il n'a pas trouvé d'évaluation publique d'Aaronson ni d'Ambainis. PSI cite des commentaires d'autres chercheurs, mais pas ceux des auteurs de la conjecture.
Une preuve écrite par IA et signée par une personne
Le dépôt détaille que les énoncés mathématiques, le premier brouillon de l'article et la formalisation en Lean « ont été produits par des modèles d'IA ». David Turturean, de PSI, a développé le système avec lequel le modèle a été exécuté, a relu l'article et figure comme responsable de sa justesse.
PSI a cité quatre chercheurs de l’Université de Stanford : Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan. Selon l’entreprise, ils ont lu la nouvelle preuve et l’ont qualifiée de « résultat énorme ». Ces commentaires sont connus par l’intermédiaire de PSI et non par une publication des auteurs eux-mêmes.
En août 2026, ces mêmes quatre chercheurs avaient démontré la prédiction de la conjecture dans un cas particulier : les algorithmes quantiques qui consultent leurs données dans un nombre fixe de tours en parallèle ne parviennent pas à obtenir un avantage exponentiel avec des entrées aléatoires. La preuve de PSI vise le cas général.
Cette annonce intervient après une autre publication d’Anthropic. Le 16 octobre, l’entreprise a annoncé que son modèle Claude avait conçu, presque sans aide humaine, des circuits quantiques qui améliorent les meilleurs publiés et qui, dans certains cas, réduisent les ressources nécessaires d’un ordre de grandeur ou plus.
Dans cette recherche, Anthropic a précisé que l’une des améliorations a rendu environ 12 fois moins coûteuse l’étape la plus onéreuse d’un algorithme d’optimisation. Une autre conception, un calcul de courbes elliptiques, est issue d’une seule exécution de 53 heures.
PSI a publié l’article, le code et les fichiers Lean sous licence Apache 2.0, afin que d’autres spécialistes puissent vérifier l’énoncé et la démonstration.