719: é esse o número de manuscritos matemáticos que a OpenAI (abre em nova aba) publicou de uma vez, em 6 de outubro de 2026, num repositório público sob licença aberta. A empresa diz que o material vem de um modelo de IA interno que atacou cerca de 4.000 problemas em aberto da matemática. A divulgação causou assombro e desconfiança na mesma semana, e a distância entre as duas reações é exatamente o que ajuda a separar fato de marketing.
O repositório, github.com/openai/math (abre em nova aba), organiza os 719 manuscritos em 372 famílias. Uma família agrupa trabalhos relacionados: um resultado principal, argumentos complementares, consequências ou provas alternativas. Isso já importa para a leitura dos números. Não são 719 descobertas independentes; são 719 documentos, parte deles desdobramentos de um mesmo resultado. Órgãos de imprensa divergiram na contagem: a New Scientist e a Quanta Magazine falaram em 722 artigos e, no caso da Quanta, em 377 questões em aberto abordadas, enquanto o próprio repositório da OpenAI lista 719 manuscritos. A diferença de três pode parecer detalhe, mas numa área em que a precisão é o produto, ela mostra por que a checagem externa ainda está em curso.
O que a máquina realmente verificou
A peça central da credibilidade do anúncio é o Lean, uma linguagem de programação em que uma prova matemática é escrita de modo que o computador confira cada passo lógico. Se o verificador aceita, a demonstração não contém falhas dentro das hipóteses declaradas. Segundo o repositório, cerca de 42% dos resultados principais (300 dos 719, na atualização de 7 de outubro) já têm essa formalização, com mais sendo adicionadas aos poucos.
Aqui está a ressalva que a OpenAI fez questão de registrar: o catálogo contém resultados "em diferentes estágios de verificação", e alguns dos não formalizados "podem ter problemas". Ou seja, quase 60% do material publicado ainda depende da leitura de matemáticos humanos para saber se está correto. A empresa prometeu corrigir com rapidez o que apresentar falhas.
A semana provou que a ressalva era necessária
Em 7 de outubro, um dia depois da publicação, o próprio repositório registrou a retirada de três manuscritos. Um erro de sinal invalidou um argumento central do artigo sobre algebraicidade de classes de Weil, e com ele dois trabalhos que dependiam daquela construção. Outros 14 manuscritos foram revisados, com reparos de prova, correções de enunciados e ajustes de hipóteses, e 13 documentos adicionais foram atualizados para citar as versões corrigidas.
Esse episódio corta nos dois sentidos. Mostra que os artigos sem formalização carregam risco real de erro, inclusive o tipo de erro bobo, um sinal invertido, que passa despercebido. E mostra também um processo de correção funcionando ao ar livre, com notícias explicando a falha e links para as versões arquivadas, num nível de transparência que raramente existe em matemática publicada por humanos.
Os especialistas ouvidos pela imprensa foram mais céticos. Johan Commelin, diretor da iniciativa Mathlib, avaliou para a Quanta Magazine que algumas formalizações parecem provar enunciados mais fracos do que os anunciados, ou apenas parte do resultado, e que a equivalência entre o que o Lean certifica e a afirmação matemática original exige especialistas humanos. Mihalis Dafermos, de Princeton, disse que vários artigos da sua área estavam escritos de forma vaga demais para constituírem uma prova que uma pessoa pudesse verificar. A revista Science registrou que os matemáticos estão divididos sobre se esse tipo de publicação em massa faz bem à área.
O modelo, o custo e o volume de fracassos
A OpenAI não nomeou o modelo responsável. O texto oficial o descreve como um "modelo de fronteira interno", não lançado, e diz que trabalha para liberá-lo de forma responsável no futuro. O repositório traz dez resumos do raciocínio do modelo e estimativas do custo computacional: cada resultado consumiu, em média, o equivalente a cerca de três horas de uso do ChatGPT Pro em modo de raciocínio, segundo a própria empresa.
O dado menos publicitado é a taxa de acerto. O modelo tentou aproximadamente 4.000 problemas e falhou na vasta maioria deles. Os 719 manuscritos são o que sobrou depois de agrupar a produção e exigir um nível de relevância. Para quem acompanha o setor, essa proporção é informativa: a máquina não resolveu matemática em série, ela produziu uma pilha de acertos a partir de uma montanha de tentativas.
A sequência de anúncios dá o contexto
A divulgação de outubro não surgiu do nada. A OpenAI vinha escalando anúncios do tipo ao longo do ano:
| Data | Anúncio | Modelo envolvido |
|---|---|---|
| Maio de 2026 | Refutação da conjectura de distância unitária de Erdős, durante avaliação | modelo não lançado |
| 1º de agosto de 2026 | 10 resultados sobre problemas antigos, com certificados em Lean | versão interna de Astra |
| 8 de setembro de 2026 | Solução alegada do problema de Navier-Stokes, prêmio do Milênio | modelo interno mais capaz que o GPT-6 Astra |
| 6 de outubro de 2026 | Catálogo com 719 manuscritos em 372 famílias | modelo interno não nomeado |
No caso do Navier-Stokes (abre em nova aba), um dos sete Problemas do Prêmio do Milênio, em aberto há cerca de 90 anos, a OpenAI alegou que seu sistema mostrou que um fluido inicialmente liso, em repouso, pode desenvolver uma singularidade em tempo finito. Segundo a empresa, os agentes chegaram à resolução em 5 de setembro, cerca de 88 horas após o início, e a formalização em Lean levou 17 horas adicionais. Vale o registro: a página é a alegação da OpenAI. O Instituto Clay, que administra os prêmios, não confirmou aceitação.
Já a divulgação de agosto, com dez resultados, incluindo novos limites superiores para empacotamento de esferas em dimensões altas, trazia um detalhe de franqueza incomum: a OpenAI estimou que o total de tokens usados custaria cerca de 2.000 dólares nas tarifas de API da época, e declarou que atribuir autoria humana a provas geradas integralmente por IA representaria uma distorção, embora humanos tenham preparado os manuscritos e assumido responsabilidade pela correção.
O que é fato, o que é alegação e o que é embalagem
Três camadas convivem nesse episódio, e confundi-las é onde o leitor se perde.
- Fato verificado: a publicação existe, é pública e está sob licença aberta. Pelo menos 300 provas principais passaram pela checagem automática do Lean, que elimina falhas lógicas dentro das hipóteses declaradas. A OpenAI publicou inclusive estatísticas de fracasso, algo raro em comunicados corporativos.
- Alegação ainda sem confirmação: a correção dos manuscritos não formalizados, a qualidade dos textos (contestada por Dafermos na área dele) e a equivalência plena entre certificados Lean e os resultados anunciados (a dúvida levantada por Commelin). A palavra da empresa basta até que matemáticos independentes digam o contrário ou concordem.
- Embalagem: titulares do tipo "722 descobertas de uma vez" exageram pela estrutura do próprio catálogo. As famílias incluem consequências e provas alternativas de um mesmo resultado, e o repositório da OpenAI lista 719 manuscritos, não 722 descobertas independentes. A comparação implícita, de que a IA resolveu setecentos problemas que travaram gerações de matemáticos, não corresponde ao que o material mostra.
Há um contraste curioso na postura da empresa. Comunicados anteriores da OpenAI, como os que circundam lançamentos de modelos, costumam operar no superlativo. Desta vez a empresa consultou um grupo consultivo independente sobre matemática e IA, ligado ao Institute for Advanced Study, seguiu recomendações públicas sobre como divulgar os resultados e publicou um repositório com protocolos de citação e revisão. A New Scientist, ao lado do tom de admiração, já chamava a operação de algo que a OpenAI precisaria "limpar". Quando o maior gerador de hype do setor publica estatísticas de derrota junto com as de vitória, o sinal misto é, ele próprio, uma notícia.
O que muda, na prática, é o ritmo da matemática como ofício. Resultados em aberto passaram a receber ataques automatizados com custo marginal por tentativa, e a comunidade recebe catálogos inteiros para auditar, com a correção acontecendo em repositório público e em tempo real. Para o matemático, o trabalho se desloca em parte para a verificação. Para o público, a lição metodológica é simples: o número grande do título mede volume de publicação, e só a formalização em Lean, que avançava de 42% em 7 de outubro, transforma volume em verdade.
Perguntas frequentes
Os problemas matemáticos foram realmente resolvidos?
Em parte. Cerca de 42% das provas principais foram formalizadas em Lean, linguagem que permite ao computador verificar a lógica, o que é uma confirmação forte. O restante depende de revisão humana, e a OpenAI admitiu que alguns desses resultados podem ter problemas. Três manuscritos já foram retirados por erro de sinal.
O que é Lean?
É uma linguagem de programação usada para escrever provas matemáticas de forma que um computador confira cada passo lógico. Uma prova formalizada e aceita pelo verificador não contém falhas de raciocínio dentro das hipóteses declaradas, o que elimina erros que uma leitura humana poderia deixar passar.
O modelo de IA que produziu esses resultados está disponível?
Não. A OpenAI o descreve como um modelo de fronteira interno, sem nome divulgado, e afirma que trabalha para lançá-lo de forma responsável no futuro. Nenhum produto à venda hoje é esse modelo.
Por que alguns artigos foram retirados?
Um erro de sinal em um manuscrito de geometria algébrica invalidou um argumento central e, com ele, dois trabalhos que dependiam daquela construção. A OpenAI retirou os três do catálogo, deixou avisos explicando a falha e revisou outros 14 manuscritos no dia seguinte.