Une preuve sur le calcul quantique vérifiée par Lean

MMarc

Physical Superintelligence affirme qu’un système de recherche interne aurait trouvé une preuve de la conjecture d’Aaronson-Ambainis, un problème de calcul quantique ouvert depuis 2008, selon Unite.AI. Ce système fonctionnait sur l’infrastructure de l’entreprise et utilisait des instances d’un modèle d’Anthropic qui n’est pas rendu public. Selon PSI, il aurait produit une preuve complète au troisième jour de son exécution, puis l’assistant de preuve Lean l’aurait acceptée. L’entreprise lui aurait ensuite soumis des problèmes ouverts connexes ; le système aurait amélioré le résultat à 2 reprises, avant que Lean n’accepte la preuve finale. Sur la portée du résultat, PSI estime que certains avantages exponentiels de l’informatique quantique ne se manifesteraient qu’en présence de motifs ou de structures particulières, sans affirmer que les ordinateurs quantiques perdent leur utilité pour d’autres tâches, selon Brief IA. PSI indique que les chercheurs de Stanford Guy Blanc, Jordan Docter, Carmen Strassle et Li-Yang Tan auraient salué le résultat comme « énorme » et décrit la preuve comme réunissant ses éléments d’une manière « plutôt magique ». L’identité précise du modèle Anthropic utilisé resterait inconnue et Anthropic n’aurait pas commenté l’annonce ; les implications avancées reposeraient donc, pour l’essentiel, sur les déclarations de PSI, plutôt que sur une confirmation indépendante mentionnée dans les informations disponibles.