Peut-on confier à une intelligence artificielle la recherche en informatique théorique, ce domaine qui s'intéresse aux limites mêmes du calcul? Une étude déposée le 5 novembre sur la plateforme de prépublications arXiv propose une réponse chiffrée, et plutôt nuancée : les meilleurs agents savent désormais démontrer des théorèmes publiés, mais aucun n'a réglé une seule des 30 conjectures ouvertes qu'on leur a soumises.
Un « examen » pour les chercheurs artificiels
Le document s'intitule TCSExam. Selon la page de la prépublication, il est signé de Yifan Luo, Zhengying Liu, Yang Yuan, Zhilin Yang et Andrew Chi-Chih Yao. Deux noms attirent l'attention. Andrew Yao est lauréat du prix Turing, décerné en 2000, selon l'ACM, pour ses contributions fondamentales à la théorie du calcul, notamment la génération de nombres pseudo-aléatoires, la cryptographie et la complexité de la communication. Zhilin Yang, lui, est cofondateur de Moonshot AI, l'entreprise chinoise derrière les modèles Kimi. Le média chinois The Paper (Pengpai) a été l'un des premiers à relayer le travail, le 9 novembre, en le décrivant comme une collaboration entre l'équipe de Yao, à l'Université Tsinghua, et Moonshot AI.
L'image choisie par The Paper est parlante : si l'informatique théorique est l'« olympiade » des mathématiques, alors il s'agissait d'y inviter des modèles de langage. Il ne s'agit pas de réparer des ordinateurs, mais de déterminer quels problèmes se calculent rapidement et où s'arrêtent les preuves possibles.
Quatre épreuves, vérifiées par la machine
L'originalité de TCSExam tient moins à la difficulté qu'à la méthode. Le référentiel compte 100 tâches : 20 théorèmes de recherche à prouver dans Lean 4, 30 problèmes d'ingénierie de solveurs évalués sur des familles d'instances, 20 problèmes de construction notés par rapport à des records documentés, et 30 conjectures ouvertes à prouver ou à réfuter.
Le point crucial est la vérification. Lean est un assistant de preuve : le noyau du logiciel accepte ou rejette une démonstration ligne par ligne, sans appel au jugement humain. Les auteurs précisent que chaque soumission est contrôlée soit par ce noyau, soit par un vérificateur exécutable propre à la tâche. Les trois types d'épreuves qui ne reposent pas sur Lean utilisent des vérificateurs automatiques, de sorte qu'aucune réponse ne dépend d'une appréciation subjective. Le dépôt GitHub du projet détaille les règles : les tâches de théorèmes demandent une preuve Lean d'un résultat publié, les constructions exigent un objet ou une borne vérifiés, et les conjectures ouvertes n'acceptent qu'une preuve ou une réfutation complète en Lean.
Une version allégée, TCSExam-Lite, retient 20 tâches, à raison de cinq par épreuve. Les auteurs affirment qu'elle réduit de 80 % le nombre de tentatives, pour un budget identique par essai. Ils ont évalué huit agents sur la version complète et neuf sur la version allégée, et le classement des deux versions est fortement corrélé (coefficient de Spearman de 0,93).
Ce que disent les résultats
Selon l'analyse de Crypto Briefing, GPT-6 Astra, d'OpenAI, prend la première place de la version complète avec un indice de 71,9, et c'est surtout la démonstration de théorèmes qui explique son avance : 14 tâches réussies sur 20, soit 70 %. Dans la version allégée, c'est Opus 5.5 qui arrive en tête, avec 72,3.
Le revers est net. Toujours selon Crypto Briefing, aucun agent n'a résolu l'une des 30 conjectures ouvertes dans l'évaluation principale : le taux de réussite est de 0 %. Les études ne sont pas pour autant stériles. Les auteurs rapportent des solveurs améliorés, des constructions meilleures que les records documentés, ainsi que des cas particuliers et des bornes vérifiés de façon indépendante, issus des tentatives sur les conjectures.
Le site FourWeekMBA, qui a lu l'article en entier, cite un exemple : en s'attaquant à une conjecture, GPT-6 Astra a démontré la conjecture d'Alon, Jaeger et Tarsi sur le corps à cinq éléments pour toutes les dimensions jusqu'à neuf, avec vérification Lean indépendante. Pour une borne sur les codes binaires, le média chinois Sina, reprenant The Paper, rapporte un résultat plus modeste en apparence : un code de longueur 22 et de distance minimale 10 compterait au plus 82 mots, contre 84 dans la littérature publiée. L'article prévient toutefois que ces « records » doivent être validés de manière indépendante.
Des précautions qui comptent
Plusieurs nuances s'imposent avant de conclure à un tournant ou à un échec. D'abord, la comparaison porte sur des systèmes d'agents, non sur des modèles nus. D'après FourWeekMBA, GPT-6 Astra a été exécuté dans Codex avec une tentative par tâche, tandis que les modèles Kimi l'ont été dans Kimi Code avec trois tentatives. Le classement mélange donc la qualité du modèle, celle de son environnement et le budget alloué.
Ensuite, la contamination des données reste un risque pour des théorèmes déjà publiés. La page du projet note que deux modèles évalués après coup, Kimi K3.1 Pro et DeepSeek V4.1 Flash 1017, disposaient d'un accès à Internet, et que leurs soumissions réussies sur certaines tâches reprenaient des contre-exemples et des preuves Lean déjà publiés, adaptés aux définitions de l'épreuve. Autrement dit, un succès n'est pas toujours une découverte.
Enfin, le fait que Moonshot AI, un concurrent des entreprises évaluées, soit coauteur et hébergeur du banc d'essai invite à la prudence. Le code et les données étant publics, d'autres équipes pourront reproduire les résultats, ce qui est la meilleure réponse à ce genre de réserve.
Un contexte de promesses et de contestations
TCSExam arrive dans une année où les annonces de mathématiques assistées par IA se sont multipliées. Selon le site Hayadan, des entreprises d'IA rapportent depuis janvier 2026 avoir résolu des dizaines de problèmes ouverts, dont beaucoup posés par Paul Erdős, certaines preuves ayant été vérifiées par des mathématiciens et dans Lean, mais les résultats les plus marquants n'ayant pas encore passé la révision par les pairs. Le 1er août, selon Quartz, OpenAI a affirmé que son prochain modèle, Astra, avait résolu dix problèmes ouverts depuis au moins dix ans, pour environ 2 000 dollars, en publiant des certificats de preuve Lean 4 sur GitHub.
Ces annonces font l'objet de débats. D'après un décompte publié par DEV Community au 26 octobre, seulement environ 42 % des principaux résultats du modèle non publié d'OpenAI disposaient de preuves vérifiées par machine, trois articles avaient été retirés le lendemain de leur parution, et la plupart des autres attendaient encore l'examen d'experts. Ce site est une source secondaire et ses chiffres sont à prendre avec réserve, mais ils illustrent l'écart entre l'annonce et la validation.
Le laboratoire Epoch AI a tenté de calibrer ces affirmations avec FrontierMath Erdős, un banc d'essai de 68 problèmes d'Erdős significatifs, ouverts en août 2026, sélectionnés par Thomas Bloom et formalisés en Lean. Selon Epoch AI, Astra y a résolu environ 3 % des problèmes dans la configuration testée, ce qui illustre des percées réelles mais encore assez rares. Un autre banc d'essai, FormalTCS, conclut que la formalisation automatique, c'est-à-dire la traduction d'un énoncé en langage naturel vers une preuve Lean rigoureuse, est le principal goulot d'étranglement des modèles actuels.
Ce que l'étude montre vraiment
Le titre de l'article chinois, qui parle de « démontrer les limites des mathématiques humaines », promet davantage que ce que contient l'étude. Rien n'indique que les modèles repoussent les frontières du calcul : leurs bornes améliorées sont des progrès ponctuels, et les grandes conjectures de la discipline restent intactes. Ce que TCSExam établit, c'est un gradient : les agents de pointe maîtrisent désormais la formalisation de résultats connus, commencent à produire de petites améliorations vérifiables, et échouent encore devant l'inédit de grande envergure.
L'intérêt durable du travail est sans doute là, dans l'outil de mesure. Un examen dont chaque réponse est tranchée par un vérificateur formel, et dont les conjectures ouvertes servent de plafond, permettra de suivre l'évolution des agents d'une génération à l'autre. Si le taux de 0 % sur les conjectures devait bouger, la preuve en serait publique, vérifiable et, pour une fois, sans interprétation possible.