Uma equipa da Universidade Tsinghua, da Moonshot AI e do Instituto Shanghai Qizhi apresentou o TCSExam, um banco de ensaio pensado para perceber se os agentes de IA conseguem fazer verdadeira investigação em ciência da computação teórica, em vez de responder a exercícios de manual. O repositório MoonshotAI/TCSExam ficou público no GitHub a 3 de novembro de 2026, sob licença Apache-2.0, e o artigo correspondente chegou ao arXiv (2611.07962) a 5 de novembro. Assinam-no Yifan Luo, Zhengying Liu, Yang Yuan, Zhilin Yang e o cientista da computação Andrew Chi-Chih Yao.
A versão completa reúne 100 tarefas revistas por especialistas e divididas em quatro trilhos. Vinte são teoremas retirados de artigos recentes da área, publicados entre 2023 e 2026, que têm de ser demonstrados em Lean 4. Trinta pedem engenharia de solvers: o agente entrega um programa reutilizável, avaliado em instâncias escondidas, com problemas oriundos de competições e bibliotecas conhecidas. Outras vinte exigem construções, como códigos, grafos ou empacotamentos, comparadas com recordes documentados. As últimas trinta são conjeturas em aberto, entre elas a do log-rank e a de Ryser, que é preciso provar ou refutar. Cada resposta passa pelo núcleo do Lean ou por um verificador executável, pelo que nenhuma nota depende de um modelo a fazer de juiz. Há ainda um subconjunto Lite, com cinco tarefas por trilho, que reduz em 80% o número de tentativas mantendo as 12 horas por tentativa.
Foram avaliados oito agentes na versão completa. O GPT-6 Astra, a correr no Codex, fica à frente no índice TCSExam com 71,9 pontos, seguido do Kimi K3.1 Pro com 57,4 e do Kimi K3 com 46,8. Mais atrás, aproximadamente entre 40 e 46 pontos, surgem DeepSeek V4.1 Flash 1017, GLM-5.3, Qwen3.8 Max e Grok 4.6. O Astra demonstrou 14 dos 20 teoremas sem lemas intermédios, uma taxa de 70%, quando nenhum rival passou dos 38,3%. Na versão Lite, que acrescenta o Opus 5.5 da Anthropic, é este que lidera com 72,3, contra 67,0 do Astra. Segundo os autores, as duas versões ordenam os oito agentes comuns quase da mesma forma, com uma correlação de Spearman de 0,93.
O capítulo das conjeturas é o mais revelador. Nenhum agente chegou, por mérito próprio, a uma resolução completa. O artigo explica sem rodeios as duas submissões aceites: o Kimi K3.1 Pro e o DeepSeek V4.1 Flash 1017, com acesso à internet, foram buscar contraexemplos e provas em Lean que a OpenAI já tinha divulgado para a conjetura de Ryser e para a chamada conjetura MIRUP, e adaptaram-nos às definições das tarefas, que tinham sido redigidas antes dessa divulgação.
Ainda assim, os ensaios produziram matemática verificada de alcance mais limitado. O GPT-6 Astra provou a conjetura de Alon-Jaeger-Tarsi sobre o corpo de cinco elementos para todas as dimensões até 9, alargando resultados anteriores que iam até 7 e 8, e os autores afirmam que uma verificação independente em Lean o confirma apenas com axiomas padrão. Nas construções, o Kimi K3 obteve um grafo de 124 vértices e 630 arestas sem ciclos de comprimento 3 ou 4, uma aresta acima da referência, e um código quântico estabilizador [[25,7,6]] que sobe a distância de 5 para 6. O Astra mostrou também que os códigos binários de comprimento 22 e distância mínima 10 não passam de 82 palavras, melhorando o limite publicado de 84.
Para quem desenvolve ou avalia agentes, o projeto tem utilidade prática. O repositório inclui as fontes das tarefas, receitas Docker e ferramentas de avaliação no formato Harbor, usa o Kimi Code por omissão e documenta configurações para Claude Code, Codex e Grok Build. Como cada resultado passa por uma verificação formal ou executável, o TCSExam distingue demonstrações reais de texto apenas convincente. Publicações independentes como On The Wire, Aivio News e Crypto Briefing já noticiaram o trabalho, sobretudo pelo contraste entre o bom desempenho nos teoremas e a coluna vazia das conjeturas.
Há reservas a ter em conta. Os números são da própria equipa e o artigo é uma pré-publicação sem revisão por pares. Dois autores trabalham na Moonshot AI, cujos modelos Kimi ficam em segundo e terceiro lugar. Os teoremas foram filtrados em ensaios-piloto, com mais de 40 problemas retirados por já terem sido resolvidos, o que os autores admitem poder enviesar comparações com o agente usado nessa triagem. Desconhece-se se os modelos viram as instâncias públicas dos solvers no treino, o Opus 5.5 só correu na versão Lite e cada valor mede um agente completo, com modelo, ambiente e ferramentas, e não um modelo isolado.