"Ontem será o dia em que uma nova era da matemática e da física matemática começou." A frase é do matemático de Harvard Michael Douglas, ouvido pela Scientific American dois dias depois de a OpenAI (abre em nova aba) publicar, em 6 de outubro de 2026, um pacote com 377 provas de questões abertas, espalhadas por 719 manuscritos. Pela primeira vez em larga escala, uma empresa de inteligência artificial despejou na comunidade científica uma quantidade de resultados teóricos que nem os especialistas conseguem digerir de uma vez.
O que foi publicado
A coleção está em um repositório público no GitHub, o site que hospeda código e documentos de projetos, com licença aberta Apache-2.0, o que permite que qualquer pessoa leia, copie e reuse o material. Os 719 manuscritos estão organizados em 372 "famílias", grupos que reúnem um resultado principal com argumentos complementares, consequências ou provas alternativas. Segundo o próprio repositório, os temas cobrem combinatória, vários ramos da geometria, teoria dos números, ciência da computação teórica, álgebra, topologia, probabilidade, mecânica estatística e física matemática.
O modelo que produziu tudo isso é interno e ainda não foi lançado, segundo a OpenAI. A empresa diz que a maioria dos resultados veio do mesmo procedimento: o modelo recebeu aproximadamente 4.000 problemas para tentar resolver, e as respostas consideradas significativas foram agrupadas no catálogo final. Em média, cada resultado consumiu o equivalente a três horas de "raciocínio" no nível Pro do ChatGPT, o plano pago mais caro do serviço.
Há exceções notáveis. A lista inclui um trabalho sobre uma região sem zeros da função zeta de Riemann, objeto central de um dos problemas mais famosos da matemática, e uma prova da Conjectura de Hodge para variedades abelianas CM, ambos feitos fora do procedimento padrão. Segundo a Scientific American, o mesmo modelo interno já havia resolvido, em setembro de 2026, o problema de Navier-Stokes, um dos sete desafios do Prêmio do Milênio, que vale um milhão de dólares.
A empresa anunciou a divulgação em sua conta oficial no X:
Estamos divulgando uma ampla gama de novos resultados matemáticos produzidos por um modelo de fronteira interno. Consultamos o Grupo Consultivo Independente sobre Matemática e Inteligência Artificial do Instituto de Estudos Avançados e nos baseamos em seus conselhos e recomendações públicas para orientar a forma de divulgar esses resultados.
Como se checa uma prova de IA
Aqui está o ponto que separa promessa de resultado comprovado. Uma prova matemática só vale se puder ser conferida, linha por linha, por outros especialistas. Com centenas de trabalhos ao mesmo tempo, essa checagem humana levaria anos: mais de três dezenas de matemáticos ouvidos pelo site The Verge usaram palavras como "avassalador", "sem precedentes" e "pura insanidade" para descrever a tarefa. Um deles contou que só a tabela de conteúdos, com cerca de 40 páginas, levou quase uma hora para percorrer.
Por isso, parte da coleção veio com uma mão na roda. Cerca de 42% dos resultados principais (300 de 719) foram "formalizados" em Lean, uma linguagem de programação na qual a matemática é escrita de um jeito que o computador consegue verificar sozinho, sem depender de paciência humana. Se a tradução da prova para o Lean está correta, a lógica do argumento é quase certamente válida, como explica o matemático do MIT Andrew Sutherland à Scientific American: ele espera que a maioria dos resultados acabe correta ou corrigível, mas avisa que alguns vão conter erros, "possivelmente sérios".
A cautela não é teórica. Em 7 de outubro, um dia depois do lançamento, a OpenAI retirou três manuscritos de geometria algébrica. O motivo, registrado no histórico do repositório, foi um erro de sinal, um sinal de menos no lugar errado, que invalidava um argumento de cancelamento e derrubava dois trabalhos dependententes. No mesmo movimento, a empresa revisou 14 outros manuscritos com correções de provas, enunciados mais claros e hipóteses ajustadas, e atualizou 13 adicionais que citavam as versões corrigidas. "Esperamos que os erros sejam bastante raros", disse um porta-voz da OpenAI ao The Atlantic.
Há ressalvas mais fundas. Johan Commelin, diretor da iniciativa Mathlib, observou à Quanta Magazine que algumas formalizações parecem provar enunciados mais fracos do que os alegados no artigo, ou cobrir apenas parte do resultado, algo que ele mesmo classificou como não confirmado em primeira mão. Mihalis Dafermos, de Princeton, disse que os textos de sua área estão "escritos num estilo muito sinóptico e parecem estar longe de constituir, por si sós, uma prova".
Quem supervisiona e por que isso importa
A divulgação não aconteceu no vácuo. A OpenAI diz ter seguido recomendações do Grupo Consultivo sobre Matemática e Inteligência Artificial (AGMAI), formado no Instituto de Estudos Avançados de Princeton por matemáticos de elite justamente para orientar como laboratórios de IA devem liberar esse tipo de resultado. Em setembro, o grupo publicou suas primeiras recomendações: divulgar com rapidez, usar canais acadêmicos estabelecidos quando possível e revelar o nome do modelo, os comandos usados e os custos de computação.
A OpenAI atendeu em parte. Publicou os resultados no GitHub com protocolos de revisão e citação, além de 10 resumos do raciocínio do modelo, estimativas de computação gasta e estatísticas de problemas tentados. Mas o modelo segue sem nome público, o que contraria o espírito da recomendação. Segundo o The Verge, o grupo é independente da empresa, e sua existência explica por que o lançamento veio organizado em famílias de resultados com instruções de navegação, e não como uma pilha solta de PDFs.
| O que os números dizem | Valor (segundo OpenAI e imprensa) |
|---|---|
| Provas de questões abertas divulgadas | 377 |
| Manuscritos no repositório | 719 (722 no lançamento, 3 retirados) |
| Famílias de resultados | 372 |
| Principais resultados formalizados em Lean | ~42% (300 de 719) |
| Problemas apresentados ao modelo | ~4.000 |
| Custo médio por resultado | 3 horas de ChatGPT Pro |
O que muda para quem faz matemática
O impacto prático tem dois lados. De um lado, o volume e a velocidade: segundo o The Atlantic, cerca de um terço das provas seria de conjecturas famosas em toda a matemática, outro terço seria significativo dentro de subcampos específicos e o restante seria resultados menores ou variantes, uma divisão que é caracterização da própria revista, não número oficial. De outro, o trabalho de verificação recai sobre a comunidade, que não pediu o pacote. "Se eu tivesse recebido isso por e-mail de um desconhecido, provavelmente teria apagado, tão mal escrito é", disse à Scientific American o matemático Roland Bauerschmidt, da Universidade de Nova York, sobre parte dos textos.
Para pesquisadores no Brasil, não há barreira de acesso ao material em si: o repositório é público, gratuito e em inglês, com licença que permite estudo e reuso. A OpenAI também anunciou que vai financiar workshops, conferências e programas especiais sobre o entendimento de grandes resultados produzidos por IA, e afirmou estar trabalhando para liberar de forma responsável o modelo que gerou as provas, um compromisso ainda sem prazo. O que continua fora do alcance público é a ferramenta em si: o modelo é interno e não liberado, então nenhum grupo externo, brasileiro ou não, pode hoje reproduzir os resultados com os mesmos meios.
A consequência mais concreta, porém, é outra. Pela primeira vez, a fila de verificação de resultados matemáticos importantes passou a ser definida pela capacidade de produção de uma IA, e não pelo ritmo de quem afielda as provas. Três manuscritos já caíram por um sinal de menos; 42% já têm o aval de um computador; o resto depende de matemáticos que, como resumiu o The Verge, vão levar anos para entender o que exatamente ganharam.
Perguntas frequentes
As provas da OpenAI já estão confirmadas?
Parcialmente. Cerca de 42% dos resultados principais foram verificados por computador em Lean, mas o resto aguarda checagem humana. Três manuscritos já foram retirados por um erro de sinal, e especialistas dizem que a verificação completa pode levar meses ou anos.
Onde os resultados estão publicados e quanto custa acessá-los?
No repositório público openai/math, no GitHub, com licença Apache-2.0. O acesso é gratuito e aberto a qualquer pessoa, incluindo pesquisadores brasileiros; os textos estão em inglês.
O que é a formalização em Lean?
É a tradução de uma prova matemática para uma linguagem de programação na qual o computador confere cada passo lógico automaticamente. Se a tradução estiver correta, a prova é considerada virtualmente sólida, ainda que o texto em inglês seja difícil de ler.
O modelo que gerou as provas está disponível?
Não. Segundo a OpenAI, o modelo é interno e ainda não lançado. A empresa afirma estar trabalhando para liberá-lo "de forma responsável", mas não divulgou data nem condições de acesso.