Na noite de 6 de outubro de 2026, a OpenAI fez algo que nenhum matemático tinha visto antes: colocou no GitHub, de uma só vez, 722 manuscritos de matemática — 372 famílias de resultados espalhadas por 17 áreas — todos escritos por um modelo de fronteira interno que ela não liberou para ninguém.

O anúncio no site é curto e direto: "estamos publicando uma ampla gama de novos resultados matemáticos produzidos por um modelo de fronteira interno". Entre as alegações do catálogo estão a chamada "quase-hipótese de Riemann" — a prova de que toda função L de Dirichlet, incluindo a função zeta, não tem zeros na faixa Re(s) > 7/8 —, as conjecturas de Mahler, um contraexemplo à conjectura do divisor de zero de Kaplansky e a conjectura dos jogos únicos de Khot.

São resultados que, um a um, dariam anos de trabalho para um time de pesquisadores. Aqui, saíram todos do mesmo modelo, na mesma noite, em um único repositório.

O que exatamente foi publicado

Os números vêm do próprio repositório, o openai/math, publicado sob a licença Apache 2.0:

  • 722 manuscritos, agrupados em 372 famílias — uma família junta um resultado principal e seus desdobramentos;
  • 17 áreas da matemática. A maior é ciência da computação teórica (40 famílias), seguida de combinatória (37) e geometria algébrica e complexa (36);
  • o modelo recebeu cerca de 4.000 problemas — a OpenAI conta que expandiu as avaliações depois que o desempenho nas provas que já existiam "saturou";
  • cada resultado consumiu, em média, o equivalente a três horas de raciocínio do ChatGPT Pro;
  • foram publicados apenas 10 resumos do raciocínio do modelo, e o texto de um dos resultados (a região sem zeros Re(s) > 11/12 da zeta) foi editado por humanos "para ficar legível".
Repositório openai/math no GitHub
O repositório openai/math: 722 manuscritos, catálogo de resultados e provas em Lean, publicados todos de uma vez em 06/10/2026 sob licença Apache 2.0.

"Verificado por computador" não é "verificado"

Dos 722 papers, 162 têm o resultado principal formalizado em Lean, uma linguagem de programação em que o computador confere a prova passo a passo, sem acreditar em quem escreveu. Essa contagem vem da leitura independente do catálogo de formalização feita pelo CellCog na noite do anúncio.

É aqui que a história fica interessante. Lean garante que a prova prova o teorema formal. Ele não garante que o teorema formal é exatamente o que o texto em linguagem humana está dizendo, nem que o resultado é novo. E ficaram fora da verificação por computador algumas das alegações mais bombásticas: o isomorfismo dos fatores de grupo livre, o expoente de irracionalidade de π ser exatamente 2 e a resposta negativa ao décimo problema de Hilbert sobre os racionais.

O próprio README do repositório avisa, com todas as letras: "alguns dos resultados não formalizados podem ter problemas".

Distribuição das 372 famílias de resultados por área e 162 de 722 papers com prova verificada em Lean
À esquerda, a fatia dos papers com prova checada por computador: 162 de 722. À direita, como as 372 famílias de resultados se distribuem pelas 17 áreas da matemática.

A distância entre publicar e entender

Aqui está o nó. A Scientific American ouviu um porta-voz da OpenAI: quase todos os resultados saíram de um único prompt para um único agente — e muitos dos novos resultados ainda não são compreendidos pelos próprios matemáticos da empresa. Numa disciplina em que a regra de ouro é que o autor entenda a própria prova, isso é uma inversão completa.

O matemático Andrew Sutherland, do MIT, resumiu o pedido da comunidade: "até que liberem o modelo e as pessoas consigam replicar os resultados, trate qualquer alegação de ter resolvido problemas com um agente em uma passada como não verificada. Devemos exigir os recibos".

Do outro lado, Daniel Litt, da Universidade de Toronto, defende o oposto: "se queremos saber as respostas dessas perguntas matemáticas, não vejo motivo para pedir que a empresa as mantenha em segredo". Para ele, liberar é melhor do que esconder.

E há o custo invisível. As três horas de computação por resultado são a conta da OpenAI. As centenas de horas de revisão — de pareceristas, pós-doutorandos e estudantes que vão ler, digerir e checar 722 manuscritos — caem no colo da comunidade, que não recebeu nada para isso.

A comissão que a OpenAI criou para se julgar

O episódio anterior explica a pressa em criar regras. Em setembro, a OpenAI anunciou a Advisory Group on Mathematics and Artificial Intelligence (AGMAI), comitê independente hospedado no Institute for Advanced Study, em Princeton, com nove nomes de peso — entre eles os medalhistas Fields Timothy Gowers e Martin Hairer, o físico Edward Witten e a matemática Melanie Matchett Wood. Nenhum deles é pago.

Duas semanas depois, em 29 de setembro, o grupo publicou suas primeiras recomendações, depois de ouvir mais de 600 respostas da comunidade. Duas frases são um tapa com luva de pelica:

"Não endossamos essa prática, e pedimos que [os laboratórios] parem de testar problemas matemáticos avançados em modelos proprietários."

"[Pedimos] que [as empresas] se abstenham de tratar o lançamento de resultados matemáticos como veículos de marketing para promover seus modelos."

A OpenAI diz ter consultado o grupo e seguido parte das recomendações: publicou a contagem de problemas, a estimativa de computação, resumos de raciocínio e os arquivos Lean. Mas três pontos ficaram de fora, por decisão da própria empresa — e ela admite: o modelo continua fechado, não há prompts publicados (só a média de computação) e os papers ficam no GitHub da OpenAI, não num repositório comunitário. O grupo pediu justamente o contrário, e a empresa respondeu à Scientific American que, embora leve as diretrizes "a sério", não está vinculada a elas.

Ilustração de um cérebro digital se dissolvendo em pontos e linhas
A enxurrada de resultados chegou numa disciplina que ainda digere o episódio anterior — e que agora tem que decidir como revisar matemática que ninguém entende por completo.

O caso Navier-Stokes, que abriu a ferida

Nada disso começou do zero. Em setembro, a OpenAI anunciou que um modelo seu havia resolvido a existência e suavidade das equações de Navier-Stokes — um dos sete problemas do Milênio, com prêmio de US$ 1 milhão. Aquele resultado veio de um enxame de 10 mil agentes trabalhando por cerca de 50 horas, custando milhões de dólares em computação.

A controvérsia veio depois. Segundo a Wired, o matemático e pesquisador da OpenAI Sébastien Bubeck contou que a empresa começou a treinar um novo modelo em 28 de agosto justamente depois de ler rumores de que a Anthropic estava perto de resolver Navier-Stokes. Em seguida, emergiu que a OpenAI teria "atropelado" o trabalho de outro time — uma colaboração entre um matemático da Universidade de Nova York e um funcionário da Anthropic — que estava no caminho. O resultado pode até estar certo; o método é o que a comunidade contesta.

Em paralelo, 25 matemáticos assinaram uma carta aberta intitulada "A Severe Misalignment of AI in Mathematics" (algo como "um grave desalinhamento da IA na matemática"), criticando os laboratórios por tratar "resolver problemas em aberto" como um simples benchmark de modelo novo. Há até quem leve o argumento ao extremo: um ensaio acadêmico publicado no arXiv, "The crisis of AI-generated mathematics", defende a oposição frontal ao uso de IA na área.

Por que isso importa para quem não é matemático

O problema exposto aqui não é matemático — é de credibilidade. Nós estamos delegando cada vez mais trabalho intelectual a máquinas que produzem respostas mais rápido do que a nossa capacidade de conferi-las. Na matemática, isso é grave mas gerenciável, porque uma prova pode ser checada por computador: é justamente por isso que os 162 papers com Lean valem mais, aos olhos da comunidade, do que os 560 sem.

Em quase todo o resto — um laudo médico, um parecer jurídico, uma análise financeira, um código em produção —, não existe um Lean. Não há como provar, de forma automática, que o resultado está certo; só o julgamento humano, que a enxurrada de resultados atropela.

Para o Brasil, que ainda engatinha na regulação e na infraestrutura de IA, a lição é prática: o gargalo da era dos modelos não é mais gerar resultado, é auditar. Quem souber construir métodos de verificação — trilhas de procedência, checagem formal, revisão rastreável — vai resolver o problema que os próprios laboratórios de fronteira ainda não resolveram. A IA já sabe escrever 722 provas numa noite. Ninguém ainda sabe como lê-las a tempo.

Fontes