Une équipe de l'université Tsinghua, de Moonshot AI et de l'institut Shanghai Qizhi a dévoilé TCSExam, un banc d'essai conçu pour mesurer si les agents d'IA savent mener de vraies recherches en informatique théorique, plutôt que résoudre des exercices de manuel. Le dépôt MoonshotAI/TCSExam est devenu public sur GitHub le 3 novembre 2026, sous licence Apache-2.0, et l'article associé a paru sur arXiv (2611.07962) le 5 novembre. Il est signé par Yifan Luo, Zhengying Liu, Yang Yuan, Zhilin Yang et l'informaticien Andrew Chi-Chih Yao.
La version complète compte 100 tâches relues par des spécialistes, réparties en quatre volets. Vingt sont des théorèmes issus d'articles récents du domaine, parus entre 2023 et 2026, à démontrer en Lean 4. Trente relèvent de l'ingénierie de solveurs : l'agent rend un programme réutilisable, noté sur des instances cachées tirées de compétitions et de bibliothèques reconnues. Vingt autres demandent des constructions, codes, graphes ou empilements, comparées à des records documentés. Les trente dernières sont des conjectures ouvertes, dont celle du log-rank et celle de Ryser, qu'il faut prouver ou réfuter. Chaque soumission passe par le noyau de Lean ou par un vérificateur exécutable, si bien qu'aucune note ne repose sur un modèle jouant le rôle d'arbitre. Un sous-ensemble Lite, avec cinq tâches par volet, réduit de 80 % le nombre de tentatives tout en conservant 12 heures par tentative.
Huit agents ont été évalués sur la version complète. GPT-6 Astra, piloté via Codex, arrive en tête de l'indice TCSExam avec 71,9 points, devant Kimi K3.1 Pro à 57,4 et Kimi K3 à 46,8. Plus loin, à peu près entre 40 et 46 points, on trouve DeepSeek V4.1 Flash 1017, GLM-5.3, Qwen3.8 Max et Grok 4.6. Astra a démontré 14 théorèmes sur 20 sans lemmes intermédiaires, soit 70 % de réussite, alors qu'aucun concurrent n'a dépassé 38,3 %. Sur la version Lite, où figure aussi Opus 5.5 d'Anthropic, c'est ce dernier qui l'emporte avec 72,3 contre 67,0 pour Astra. D'après les auteurs, les deux versions classent les huit agents communs de façon presque identique, avec une corrélation de Spearman de 0,93.
Le volet des conjectures est le plus parlant. Aucun agent n'a abouti, par ses propres moyens, à une résolution complète. L'article détaille sans détour les deux soumissions acceptées : Kimi K3.1 Pro et DeepSeek V4.1 Flash 1017, qui disposaient d'un accès à Internet, ont récupéré des contre-exemples et des preuves Lean déjà publiés par OpenAI pour la conjecture de Ryser et pour la conjecture dite MIRUP, puis les ont ajustés aux énoncés des tâches. Ces tâches avaient été rédigées avant la publication d'OpenAI.
Les essais ont tout de même produit des mathématiques vérifiées, à une échelle plus modeste. GPT-6 Astra a prouvé la conjecture d'Alon-Jaeger-Tarsi sur le corps à cinq éléments pour toutes les dimensions jusqu'à 9, prolongeant des résultats qui s'arrêtaient à 7 puis à 8 ; selon les auteurs, une vérification Lean indépendante le confirme avec les seuls axiomes standard. Côté constructions, Kimi K3 a trouvé un graphe de 124 sommets et 630 arêtes sans cycle de longueur 3 ou 4, soit une arête de plus que la référence, ainsi qu'un code quantique stabilisateur [[25,7,6]] qui fait passer la distance de 5 à 6. Astra a également établi que les codes binaires de longueur 22 et de distance minimale 10 contiennent au plus 82 mots, contre une borne publiée de 84.
Pour les équipes qui conçoivent ou évaluent des agents, l'intérêt est aussi pratique. Le dépôt fournit les sources des tâches, des recettes Docker et des outils d'évaluation au format Harbor ; il utilise Kimi Code par défaut et documente les réglages pour Claude Code, Codex et Grok Build. Comme chaque résultat subit un contrôle formel ou exécutable, TCSExam distingue les vraies démonstrations d'une prose simplement convaincante. Des médias indépendants, dont On The Wire, Aivio News et Crypto Briefing, ont relayé l'étude en insistant sur l'écart entre la réussite en démonstration et la colonne vide des conjectures.
Quelques réserves s'imposent. Les scores sont ceux de l'équipe elle-même et l'article reste une prépublication non relue par des pairs. Deux auteurs travaillent chez Moonshot AI, dont les modèles Kimi occupent les deuxième et troisième places. Les théorèmes ont été triés lors d'essais pilotes, plus de 40 problèmes ayant été écartés après avoir été résolus, ce qui, reconnaissent les auteurs, peut fausser la comparaison avec l'agent utilisé pour ce tri. On ignore si les modèles ont vu les instances publiques des solveurs pendant leur entraînement, Opus 5.5 n'a été testé que sur la version Lite, et chaque chiffre mesure un agent complet, modèle, environnement et outils compris, plutôt qu'un modèle seul.