Le théorème a un responsable

10 novembre 2026 · Lecture ≈ 5 min · Jules Thomas

Ce qui a été annoncé

La conjecture d'Aaronson et Ambainis pose une question simple : un ordinateur quantique peut-il être exponentiellement plus rapide qu'un ordinateur ordinaire sur des données quelconques, sans le motif caché qu'exploite par exemple l'algorithme de Shor ? Ouverte depuis 2008 selon PSI, la conjecture serait désormais un théorème : non, pas sans structure, du moins si l'on compte les lectures des données.

Un système de recherche maison a tourné sur les machines de PSI, et « Instances of a non-public Anthropic model were used in the run ». La preuve complète est apparue « during the third day of the run ». Lean, un assistant de preuve où un ordinateur vérifie chaque étape, l'a acceptée. Un conseiller de PSI, Jim Halverson, a audité la preuve. Quatre chercheurs de Stanford, qui avaient réglé un cas particulier en août, la relisent et en préparent une version courte. PSI rapporte leur message : « This is a huge result. »

Ce qu'on ne sait pas. Tout vient de PSI, une entreprise à qui l'annonce sert aussi de vitrine. Les pages news et research d'Anthropic n'en disaient rien le 9 novembre. Le modèle n'est jamais nommé. Le papier est une prépublication sur GitHub, non un article paru en revue.

La phrase rare

Dans la rubrique « Contributions », David Turturean, de PSI, a construit le système, cadré le problème, lancé le calcul, puis « prompted the model to package the results into a first draft of the paper, reviewed the draft and is responsible for the paper's correctness ». Le papier ajoute, dans son avertissement sur l'IA : « The mathematical statements in this paper were produced by AI models. »

Pourquoi un responsable, si Lean a tout vérifié ? Parce que Lean n'a pas tout vérifié, et le dépôt le dit lui-même. Sa section « What these checks do not cover » énumère les angles morts. L'énoncé d'abord : que la formule écrite en Lean dise bien ce que dit la conjecture, c'est « for a reader to confirm ». Le papier ensuite : « not itself machine-checked ». Les fondations, enfin, sont tenues pour fiables. Sur un projet témoin, le dépôt montre même qu'un énoncé faux, glissé en coupant la vérification, passe la compilation ordinaire : seules les relectures par le noyau l'arrêtent.

Le logiciel vérifie que la preuve prouve l'énoncé. Il ne vérifie pas que l'énoncé est le bon. Là où la vérification s'arrête, un nom revient.

Le nom qui revient

Michel Foucault a décrit ce va-et-vient en 1969, dans sa conférence « Qu'est-ce qu'un auteur ? ». Au Moyen Âge, un texte de médecine ou de cosmologie ne valait que signé : « Hippocrate a dit », « Pline raconte ». Puis, au XVIIe ou au XVIIIe siècle, un chiasme : on reçoit les discours scientifiques pour eux-mêmes, « dans l'anonymat d'une vérité établie ou toujours à nouveau démontrable ». Le nom de l'inventeur ne sert plus, dit-il, qu'à « baptiser un théorème ».

PSI pousse le chiasme au bout. Dans le code, le théorème s'appelle aaronson_ambainis, du nom de ceux qui l'ont conjecturé. La preuve vient d'un modèle sans nom. Et elle est « toujours à nouveau démontrable » au sens propre : une commande la fait revérifier par la machine. Pourtant, un nom revient, qui n'est pas celui d'un auteur. Foucault l'écrit : « un contrat peut bien avoir un garant, il n'a pas d'auteur ». Il rappelle aussi que les textes ont commencé à avoir des auteurs « dans la mesure où l'auteur pouvait être puni ». Le responsable est celui qu'on tiendra pour fautif si l'énoncé se révèle faux.

L'autre façon de signer

Onze jours plus tôt, OpenAI avait choisi une autre manière. Le 26 octobre, son dépôt GitHub a ajouté une prépublication au titre sans détour, « The Exponential Time Hypothesis is False » : un algorithme qui réfuterait une hypothèse classique de la théorie de la complexité. Auteur : « OpenAI ». Le dépôt présente ses textes comme produits par « an unnamed internal OpenAI model », à lire comme « a form of raw research data, rather than polished academic papers », et prévient : « We defer to the math community completely on matters of credit, precedence, and concurrent work. » Dans les fichiers que j'ai lus, aucun humain ne signe ce papier ni n'en répond.

Ce n'est pas de la désinvolture. Le même jour, OpenAI annonce qu'un groupe indépendant mené par Russell Impagliazzo, Ramamohan Paturi et Ryan Williams « will examine and explain the proof », et que tout est publié à la demande du groupe. Le 7 octobre, OpenAI avait retiré trois manuscrits après une erreur de signe, chacun avec sa notice. Sa fiche Lean reconnaît que la machine vérifie une borne moins fine que celle du manuscrit, mais toujours sous-exponentielle.

Deux régimes. Chez PSI, une personne répond et des spécialistes relisent. Chez OpenAI, l'institution publie, la communauté juge, et les erreurs se corrigent par versions. Le second passe mieux à l'échelle, avec 721 manuscrits au dépôt, mais il laisse une question sans adresse. Si l'énoncé est faux, qui a eu tort ? Une marque.

Le métier qui reste

La machine trouve, le logiciel vérifie. Il reste deux gestes qu'aucun des deux ne fait : lire l'énoncé pour s'assurer qu'il dit ce qu'on croit, et accepter d'avoir tort en public. Le premier est un métier. Le second est une signature.

Le théorème porte deux noms, la preuve aucun, le papier un seul. C'est le seul qu'on peut appeler.