GPT-6 Astra a trouvé la preuve d’une conjecture mathématique vieille de 24 ans avec de simples requêtes

Le 29 octobre, deux mathématiciens de l’université de Cambridge ont mis en ligne la preuve d’une conjecture posée en 2002. Leur résumé présente l’article comme « une digestion humaine d’une preuve de la conjecture d’isométrie spectrale pour les C*-algèbres trouvée par GPT-6 Astra ». Selon leur déclaration sur l’IA, le modèle a trouvé cette preuve « après une suite de requêtes simples ».

Le même jour, une équipe emmenée par le Pacific Northwest National Laboratory a publié un test sur 200 conjectures ouvertes tirées au hasard dans les articles de mathématiques parus sur arXiv cette année. Trois modèles GPT ont proposé une preuve ou un contre-exemple pour environ 60 % d’entre elles, pour un coût médian de 0,41 à 1,71 dollar par tentative.

Une question posée en 2002

Le problème porte sur les C*-algèbres, une famille d’algèbres d’opérateurs. Chaque élément d’une telle algèbre possède un rayon spectral : la plus grande valeur absolue de son spectre. Une isométrie spectrale est une application linéaire entre deux de ces algèbres qui conserve le rayon spectral de chaque élément.

La conjecture demande si conserver ce seul nombre pour chaque élément oblige l’application à conserver aussi les carrés. Elle affirme qu’une isométrie spectrale surjective qui envoie l’unité sur l’unité est forcément un isomorphisme de Jordan, c’est-à-dire une bijection telle que l’image de a² soit le carré de l’image de a.

Martin Mathieu et G. J. Schick, de l’université Queen’s de Belfast, en ont fait la conjecture 4.6 de leur article « First results on spectrally bounded operators », paru en 2002 dans Studia Mathematica. Mathieu l’a reprise comme problème 5 dans un recueil de questions ouvertes mis en ligne en 2008. Des résultats partiels ont suivi : le cas commutatif, les algèbres de von Neumann proprement infinies (Mathieu et Schick, 2003), puis les C*-algèbres unitaires de rang réel nul sans état tracial (Mathieu, 2020).

Le rôle du modèle et celui des auteurs

Matthew J. Colbrook, du département de mathématiques appliquées et de physique théorique de Cambridge, et George Stepaniants, de Cambridge et du Courant Institute (université de New York), la démontrent « pour des C*-algèbres unitaires arbitraires » dans une prépublication de neuf pages. Une fois la preuve trouvée par GPT-6 Astra, ils ont, selon leur déclaration, « rédigé l’article après avoir discuté plus avant de la preuve avec ChatGPT 6 pour en comprendre les mécanismes sous-jacents ». ChatGPT 6 n’a servi ensuite qu’à de légères corrections de langue.

L’article affirme que « le résultat a été formellement vérifié en Lean », l’assistant de preuve qui contrôle chaque étape logique par ordinateur. La formalisation a été déposée sur GitHub le 28 octobre, sous licence Apache 2.0, avec les énoncés et les preuves dans des fichiers séparés, un rapport sur les axiomes et un contrôle par comparaison en mode « paranoid ». Le même jour, d’après le journal GitHub Actions, sa vérification automatique en Lean a réussi. Nous n’avons pas compilé le projet nous-mêmes.

Le README précise que « l’aide de l’IA a servi à la formalisation en Lean, à sa vérification et à sa relecture » et qu’elle « n’a pas servi à rédiger le manuscrit ». La preuve formelle s’appuie sur Mathlib et sur ce que les auteurs appellent « la formalisation des algèbres d’opérateurs d’OpenAI ». À bien plus grande échelle, nous racontions le 29 octobre comment Axiom a converti avec des agents IA une preuve de 15 000 pages en code vérifié par ordinateur, en 24 jours.

200 conjectures tirées au hasard

Helen Jenne, Davis Brown, Jesse He et Henry Kvinge, du PNNL et des universités de Pennsylvanie, de Californie à San Diego et de Washington, ont voulu mesurer la fréquence de tels résultats hors des succès isolés. Selon leur article, « Beyond Selected Breakthroughs », n’étudier que les grandes percées du moment donne « une image incomplète ».

Ils ont constitué OpenConjecture à partir des articles de mathématiques déposés sur arXiv depuis février 2026, puis tiré 200 articles au hasard et une conjecture dans chacun. GPT-5.6 Sol a fait la première tentative, avec l’article complet, la recherche web et la consigne de « faire une tentative soutenue pour prouver ou réfuter » la conjecture. Les problèmes restés sans réponse sont passés à GPT-5.6 Sol Pro, puis à GPT-6 Astra Pro, sans recherche web ; tous les essais ont utilisé l’effort de raisonnement xhigh, sans aide propre au problème.

Les modèles ont proposé des contre-exemples à 70 conjectures et des preuves pour 55 autres, soit 125 sur 200. La première passe a fourni 82 de ces réponses, la deuxième 26 et la troisième 17 ; à la troisième passe, les preuves dépassaient les contre-exemples. La consommation médiane de jetons revenait à environ 0,97, 0,41 et 1,71 dollar par tentative selon la passe, « au moment de la rédaction » (0,87, 0,37 et 1,53 euro au cours de la BCE du 30 octobre 2026).

Une nouvelle instance du même modèle a ensuite relu chaque réponse, et 84 % ont passé ce contrôle. Une relecture par le modèle a classé environ 60 % des contre-exemples validés des deux premières passes comme « prêts à l’emploi », le genre d’objet qu’un spécialiste essaie en premier. Ceux de la troisième passe reposaient en général sur des modifications non triviales, et l’article conclut que certaines résolutions montrent « une nouveauté au moins modérée ».

Le reste de la semaine sur arXiv

Le Ramanujan Challenge, organisé par le groupe Ramanujan Machine du Technion, à Haïfa, a publié ses résultats le même jour. Le concours s’est tenu de juillet à août 2026 autour de dix problèmes de théorie des nombres : huit résultats démontrés par les organisateurs mais jamais publiés, et deux conjectures ouvertes.

Les participants ont envoyé 228 contributions : 4 802 pages de preuves et 1 079 380 lignes de code en Lean, Python, Mathematica et Sage. L’une des deux conjectures a reçu une preuve correcte formalisée en Lean et plusieurs autres preuves probablement correctes ; la seconde reste ouverte. Les meilleures preuves en langage naturel venaient de contributions utilisant des modèles Claude et GPT. Parmi les auteurs de solutions correctes figure « une personne sans formation mathématique supérieure », qui a résolu l’un des problèmes plus simplement que les organisateurs.

En physique, Valentin Link, de l’université technique de Berlin, a montré le 27 octobre que TEMPO, une méthode de simulation des systèmes quantiques qui interagissent avec leur environnement, peut s’appuyer sur un réseau dont la taille interne ne dépend plus de celle du système, ce qui, selon lui, ouvre la méthode aux grands systèmes. Son résumé précise : « Cette structure a été découverte par Claude Opus 5.5 lors d’un développement d’algorithme guidé. »

Le 22 octobre, nous rapportions déjà que trois équipes avaient déposé des preuves d’une conjecture de géométrie vieille de 31 ans, toutes avec l’IA, puis le 26 octobre que six revues de probabilités suspendaient les nouvelles soumissions face à un afflux lié en grande partie à l’IA.

Les limites posées par les auteurs

Les trois articles de mathématiques sont des prépublications, et aucun n’a été évalué par des pairs. Le résultat de Cambridge repose sur la rédaction des auteurs et sur leurs fichiers Lean, eux-mêmes produits avec l’aide de l’IA.

L’équipe du PNNL encadre son chiffre principal : ses décomptes « ne doivent pas être interprétés comme des taux de problèmes ouverts nouvellement résolus ». Aucun expert n’a vérifié les 125 réponses, et l’article prévient que « le modèle solveur et le modèle relecteur peuvent partager des erreurs mathématiques ».

Certains contre-exemples s’en tiennent à la lettre d’une conjecture et en manquent l’intention : le groupe trivial opposé à une conjecture de théorie des nombres, ou un graphe à un seul sommet que le modèle qualifiait lui-même de « contre-exemple littéral ». Plusieurs preuves de la première passe portaient sur des conjectures déjà tranchées dans des prépublications ultérieures, et seuls des modèles GPT ont été testés, une fois chacun. Les organisateurs du Ramanujan Challenge écrivent que les solutions à leurs conjectures « n’ont pas encore été entièrement évaluées ».

Notre analyse

Dans chacun de ces articles, la vérification des résultats est l’étape lente. À Cambridge, GPT-6 Astra a produit l’argument après des requêtes simples, et les deux auteurs ont consacré leur travail à le comprendre, à le rédiger et à le faire passer en Lean. Le groupe du Technion décrit la même contrainte : « à mesure que les systèmes d’IA produisent des résultats mathématiques et scientifiques plus vite que les experts ne peuvent les vérifier, la validation devient un goulot d’étranglement central ».

L’échantillon aléatoire répond à l’objection habituelle, celle des exemples triés sur le volet. Sur 200 conjectures que personne n’a choisies, les modèles ont proposé une réponse pour la majorité d’entre elles, pour un coût médian inférieur à deux dollars par tentative. L’étude ne dit pas pour autant combien de ces réponses sont justes ou nouvelles, et ses auteurs demandent d’évaluer aussi « la fidélité à l’énoncé voulu, l’attribution et la nature de la contribution mathématique ».

Trois éléments diront ce qui tient : la relecture par des experts des 125 réponses d’OpenConjecture, l’avis des rapporteurs de revue sur la preuve de Cambridge et l’évaluation des solutions aux conjectures que les organisateurs du Technion annoncent « dans les semaines à venir ».

Sources

• Spectral isometries of unital C*-algebras, Matthew J. Colbrook et George Stepaniants, arXiv, 29 octobre 2026
• A proof of the spectral isometry conjecture for C*-algebras (Lean formalization), Matthew J. Colbrook et George Stepaniants, GitHub, 28 octobre 2026
• First results on spectrally bounded operators, M. Mathieu et G. J. Schick, Studia Mathematica, 2002
• A Collection of Problems on Spectrally Bounded Operators, Martin Mathieu, arXiv, 15 octobre 2008
• Beyond Selected Breakthroughs: Evaluating Language Models on Randomly Sampled Mathematical Conjectures, Helen Jenne, Davis Brown, Jesse He et Henry Kvinge, arXiv, 29 octobre 2026
• Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs, Alan Sorani et al., arXiv, 29 octobre 2026
• The TEMPO network can be made independent of the system size, Valentin Link, arXiv, 27 octobre 2026

Image d’en-tête : graphique MACCUS, données de l’étude OpenConjecture (Jenne, Brown, He et Kvinge, arXiv:2610.40382, 29 octobre 2026)