Le 6 novembre, la start-up PSI (Physical Superintelligence) a annoncé que son système de recherche interne, fonctionnant avec un modèle Anthropic non publié, a prouvé la conjecture d'Aaronson-Ambainis, ouverte depuis 18 ans. La preuve complète a été rédigée le troisième jour de l'exécution et a passé la vérification pas à pas de Lean, un assistant de preuve qui contrôle chaque étape. C'est une affirmation marquante pour l'IA s'attaquant aux mathématiques difficiles — mais pour l'instant, cela reste l'affirmation d'une seule entreprise : l'article n'a pas été évalué par des pairs.
Que demande réellement cette conjecture ?
La conjecture d'Aaronson-Ambainis demande de combien les ordinateurs quantiques peuvent être plus rapides que les ordinateurs classiques sur des données non structurées. Elle affirme que, sur des entrées non structurées, les algorithmes quantiques ne peuvent pas atteindre d'accélération exponentielle. La question est ouverte depuis 2008. En août, une équipe de Stanford en a prouvé un cas particulier ; PSI affirme que son système a désormais étendu le résultat au cas complet. Si la preuve tient, elle trace une limite nette autour de ce que l'informatique quantique peut faire.
Comment la machine a-t-elle prouvé, et combien de fois a-t-on vérifié ?
Selon PSI, le système de recherche a tourné en continu sur l'infrastructure de l'entreprise, a rédigé une preuve complète le troisième jour, puis a amélioré le résultat à deux reprises sur des problèmes connexes, Lean acceptant la version finale à chaque fois. PSI a publié l'article et la formalisation Lean 4 ensemble sur GitHub : 648 théorèmes vérifiés par machine, aucune étape de preuve laissée vide, aucun axiome supplémentaire introduit ; les énoncés ont également été rejoués via le noyau Lean et l'implémentation indépendante lean4lean. David Turturean, membre du personnel technique de PSI, répond de l'exactitude de l'article, et des mathématiciens ont audité la preuve.
Ne l'inscrivons pas encore dans les manuels
Une preuve vérifiée par machine n'équivaut pas à une acceptation par la communauté mathématique. Lean ne peut garantir que chaque étape suit les règles, mais pas confirmer que l'énoncé formalisé correspond à la conjecture telle qu'Aaronson et Ambainis l'ont posée à l'origine — cela demande encore une vérification manuelle par des experts ; le texte lisible par l'homme n'a pas lui-même été vérifié par machine ; la preuve compte les requêtes, pas le temps de calcul total ; et le modèle utilisé n'a pas été divulgué, Anthropic ayant refusé de commenter. Toujours le 6 novembre, Google DeepMind a annoncé que des agents IA avaient trouvé deux nouvelles faiblesses dans le chiffrement RSA 1024 bits. L'IA avance à la fois en mathématiques et en cryptographie. La question de savoir si la preuve de PSI résistera à l'examen des pairs sera tranchée par les expertises des prochaines semaines.
