Quantique : une IA a résolu un problème ouvert depuis 2008, qu'est-ce que ça change ?

Dix-huit ans. C'est le temps pendant lequel les meilleurs spécialistes de l'informatique quantique ont buté sur un même problème de maths. Et vendredi 6 novembre, une petite boîte américaine, Physical Superintelligence, annonce que c'est réglé. Pas par un génie enfermé dans un bureau : par une IA, en trois jours de calcul. Et pas n'importe laquelle, puisque c'est un modèle d'Anthropic pas encore sorti, le cousin de celui avec qui je code tous les jours. Alors là, je ne vais pas faire le blasé.

Le problème datait de 2008, et une IA l'a bouclé en trois jours

Parce qu'on parle souvent d'IA qui « résolvent des maths », et la plupart du temps c'est une machine qui refait vite ce qu'on savait déjà. Ici, c'est l'inverse : des chercheurs de Stanford n'en avaient réglé qu'un morceau cet été, et l'IA rend une preuve complète, contrôlée par un logiciel qui ne laisse rien passer. C'est exactement ce que j'attends d'une IA depuis des années : qu'elle trouve ce que personne n'avait trouvé.

La question, c'était quoi ?

En 2008, deux chercheurs, Scott Aaronson et Andris Ambainis, posent un pari. Tout le monde rêve d'ordinateurs quantiques qui iraient des milliards de fois plus vite que les nôtres. Eux se demandent : est-ce que c'est vrai pour n'importe quel problème, ou seulement pour certains ?

Prends une machine qui doit répondre par oui ou par non en lisant un énorme paquet de données. Leur intuition : si ces données sont du pur hasard, sans aucun motif caché, l'ordinateur quantique ira peut-être plus vite, mais jamais de façon astronomique. L'écart peut être gros, il ne devient jamais délirant. Le vrai coup de turbo, le gain gigantesque, il ne l'obtient que quand les données ont une structure, un motif qui se répète, une régularité qu'il peut exploiter.

C'est d'ailleurs comme ça que marche le fameux algorithme de Shor, celui qui fait trembler les banques parce qu'il saurait casser une partie des codes secrets d'Internet : il repère un motif qui se répète dans les nombres, et il en profite. Sur un tas de données sans aucun ordre, pas de miracle.

À gauche, un motif qui se répète : l'ordinateur quantique trouve un raccourci. À droite, du hasard : pas de miracle

Le hic, c'est que pendant dix-huit ans, personne n'a réussi à le démontrer. Tout le monde y croyait, des tas de cas particuliers tenaient, mais la preuve générale résistait. En 2019, Scott Aaronson avait même titré un billet de son blog « La conjecture d'Aaronson-Ambainis (2008-2019) », comme une pierre tombale, après une preuve annoncée par deux autres chercheurs. Elle n'a pas tenu, et la question était encore ouverte cet été.

Trois jours de calcul, et un correcteur qui ne laisse rien passer

Ce que raconte Physical Superintelligence, c'est un système de recherche maison qui fait tourner plusieurs copies du modèle d'Anthropic en parallèle. Elles fouillent les articles déjà publiés, proposent des idées, combinent des approches, testent des raisonnements et jettent ceux qui ne tiennent pas. Le chercheur qui pilotait le tout, David Turturean, a choisi le problème, lancé la machine, puis relu et retouché le brouillon. Le troisième jour, la preuve complète était là.

Et le plus beau, c'est en chemin : l'IA est partie d'un plan proposé par deux chercheurs, Shachar Lovett et Jiapeng Zhang, qui butait sur une inégalité qu'ils n'avaient jamais pu prouver. Elle a découvert que cette inégalité était fausse dans sa forme générale, et elle en a trouvé une autre, vraie, qui fait le même travail. Puis on l'a relancée sur des problèmes voisins, et elle a encore amélioré son propre résultat deux fois. Pchhh. Et moi qui relis encore chaque fichier que me rend Claude Code !

Maintenant, une preuve de maths écrite par une IA, ça peut aussi être un beau charabia qui a l'air juste. J'en parlais il y a un mois avec l'IA d'OpenAI qui avait résolu 372 problèmes, mais dont personne ne comprenait les preuves. Ici, la différence, c'est Lean, un logiciel qui vérifie un raisonnement mathématique ligne par ligne, comme le prof de maths le plus pénible du monde : pas de « il est évident que », pas de « on admet », chaque étape doit être justifiée jusqu'au bout ou il refuse tout. Lean a accepté la preuve. Puis la version améliorée. Et l'équipe a refait la vérification avec un deuxième vérificateur, écrit par d'autres, pour être sûre que ce n'était pas Lean lui-même qui se trompait.

Lean contrôle chaque étape de la preuve, sans exception

Détail qui m'a fait sourire : tout est en ligne, sur GitHub, et n'importe qui peut relancer la vérification chez lui. Il faut juste prévoir 173 Go de mémoire si tu es pressé, à peu près dix fois ce qu'a un bon PC de bureau, ou une machine plus modeste et onze minutes de patience. Ça reste moins long que d'attendre l'avis d'un comité de relecture.

Mouais, il y a quand même des astérisques

Bon, soyons honnêtes deux minutes. Pour l'instant, c'est l'annonce d'une entreprise, avec un manuscrit qui n'est passé devant aucune revue scientifique. Aaronson et Ambainis eux-mêmes n'ont rien dit publiquement. Les chercheurs de Stanford qui avaient réglé le cas particulier en août lisent la preuve et préparent une version plus courte pour les spécialistes, et leur premier avis est enthousiaste : « Tout s'assemble d'une façon assez magique ». Mais une lecture enthousiaste n'est pas encore une validation.

Et Lean ne garantit que ce qu'on lui donne à vérifier. Il faut encore que des humains confirment que l'énoncé tapé dans Lean dit bien la même chose que la conjecture d'origine. L'un des quatre théorèmes s'appuie aussi sur un résultat publié par d'autres chercheurs, qui n'a pas été vérifié par la machine. Rien de suspect là-dedans, c'est comme ça que travaillent tous les mathématiciens, mais ça veut dire que le « 100 % vérifié » a une petite note de bas de page.

Dernière précision, pour ne pas lui faire dire n'importe quoi : le résultat compte combien de fois la machine doit LIRE les données, pas son temps de calcul total. Il ne dit pas que les ordinateurs quantiques ne servent à rien, il dit où chercher.

Bon, et ça sert à quoi pour toi ?

Je sais, un théorème sur des polynômes, ça ne change pas la vie de ta famille demain matin. Mais il y a trois choses qui te concernent.

D'abord, ton argent. Les ordinateurs quantiques avalent des milliards, et une partie vient de tes impôts : rien qu'en France, le plan national annoncé en 2021 pèse 1,8 milliard d'euros. Et on te les vend souvent comme des machines qui accéléreront tout. Ce théorème dit noir sur blanc que non : ton tableur, ta recherche Google ou ton jeu vidéo ne tourneront pas mille fois plus vite grâce à eux. Ces machines seront utiles là où il y a une structure à exploiter, comme la chimie des médicaments, les batteries de ta voiture électrique ou certains codes secrets. Savoir où ne pas chercher, ça évite de brûler de l'argent. Et c'est exactement la question que se pose la DARPA, qui teste six machines pour savoir si l'une d'elles sera un jour rentable.

Ensuite, et c'est pour moi le plus important, la confiance. Le jour où une IA sait produire une preuve qu'un logiciel vérifie tout seul, on peut imaginer des programmes livrés avec leur démonstration, pas juste avec des tests. Ça existe déjà à petite échelle : le métro automatique de la ligne 14, à Paris, roule sans conducteur depuis 1998 avec un logiciel de sécurité démontré mathématiquement avant sa mise en service. Sauf que ça avait coûté des années de travail à des spécialistes. Si une IA fait ce travail en quelques jours, ce genre de garantie pourrait arriver dans les freins de ta voiture, la pompe à perfusion de l'hôpital ou le logiciel de ta banque.

Un métro sans conducteur dont le logiciel de sécurité a été démontré avant de rouler

Enfin, la recherche elle-même. Des problèmes bloqués depuis des décennies pourraient tomber les uns après les autres, avec une IA qui cherche et des humains qui vérifient. Il y a un précédent qui rassure : en 1976, le théorème des quatre couleurs (on peut colorier n'importe quelle carte avec seulement quatre couleurs sans que deux pays voisins aient la même) a été démontré avec l'aide d'un ordinateur, et une bonne partie des mathématiciens avait hurlé à la triche. En 2005, la preuve a été vérifiée entièrement par un logiciel du même genre que Lean, et plus personne ne la conteste.

L'échéance, honnêtement ? Pour les ordinateurs quantiques utiles, on parle de dix ans, peut-être plus. Pour des logiciels du quotidien livrés avec leur preuve, je n'ose pas donner de date. Mais pour les mathématiques, ça a déjà commencé, et c'était vendredi.

Perso, je trouve ça énorme. Une machine qui démontre ce que des humains n'avaient pas réussi à démontrer, et qui accepte de se faire contrôler ligne par ligne, c'est le rêve. Et à Anthropic : le modèle qui a fait ça, vous nous le sortez quand ? Parce que mes trois sessions de Claude Code l'attendent de pied ferme !

Sources

• Physical Superintelligence, 6 novembre 2026 : une preuve de la conjecture d'Aaronson-Ambainis (en anglais)
• GitHub : le manuscrit et la vérification Lean, avec ses réserves
• The Quantum Insider, 6 novembre 2026 : une preuve assistée par IA règle une vieille question sur les accélérations quantiques
• Scott Aaronson, novembre 2019 : la conjecture d'Aaronson-Ambainis (2008-2019)

Article écrit avec l'aide de Claude Code, relu et corrigé par moi.