A OpenAI publicou em 6 de outubro, no GitHub, 722 manuscritos de matemática produzidos por um modelo de fronteira interno, ainda não lançado. Um dia depois, em 7 de outubro, retirou três deles: uma auditoria interna achou um erro de sinal que derrubou o argumento de um artigo e a construção de outros dois que dependiam dele. Outros 14 foram revisados. Matemáticos ouvidos pela Retraction Watch e pelo TechCrunch cobram mais rigor. Só cerca de 42% dos resultados tinham prova verificada por máquina, segundo o Implicator.ai.
Em resumo
- Publicação: 722 manuscritos em 372 famílias de resultados, de cerca de 4 mil problemas testados, com média equivalente a três horas de raciocínio do ChatGPT Pro por resultado aceito.
- Retirada: em 7/10 a OpenAI tirou três artigos por um erro de sinal e revisou outros 14. O catálogo passou a 719 manuscritos.
- Verificação: 300 dos 719 resultados principais, cerca de 42%, tinham prova formal em Lean em 7/10, segundo o Implicator.ai.
- Regras da área: um grupo de matemáticos do Institute for Advanced Study publicou diretrizes em 29/09. A OpenAI seguiu parte delas.
- Leitura: o modelo produz resultados em escala, mas a checagem humana e formal ainda não acompanha esse ritmo.
O que a OpenAI publicou?
O repositório reúne 722 manuscritos agrupados em 372 famílias. Cada família junta um resultado principal, consequências ou provas alternativas, por isso 722 artigos não querem dizer 722 problemas resolvidos, como a Exame explicou. Os temas vão de teoria dos números e complexidade computacional a geometria e física matemática. O Interesting Engineering cita um resultado sobre o expoente de irracionalidade de pi e trabalhos sobre problemas NP-difíceis.
A OpenAI diz que testou cerca de 4 mil problemas. Em média, cada resultado aceito gastou computação equivalente a três horas de raciocínio do ChatGPT Pro. A Exame lembra que a conta compara recursos e não significa que um usuário comum repetiria o resultado nesse tempo. O pacote traz 10 resumos do raciocínio do modelo, regras para citação e revisão dos artigos e provas formais em Lean, um assistente de provas que permite ao computador checar cada passo. A empresa não deu nome ao modelo e diz que trabalha para liberá-lo.
Por que três artigos foram retirados?
Em 7 de outubro a OpenAI retirou os manuscritos sobre classes de Weil em variedades abelianas de dimensão oito, sobre correspondências de Kuga-Satake em superfícies K3 e sobre a conjectura de Hodge racional para produtos de superfícies K3. Um erro de sinal no primeiro invalidou o argumento dele e a construção usada pelos outros dois. A empresa também revisou 14 manuscritos, com reparo de provas, enunciados corrigidos e hipóteses mais claras, e atualizou referências em outros 13, segundo o Implicator.ai.
Um porta-voz disse à Retraction Watch que os erros apareceram numa auditoria interna, que o processo é iterativo e que a empresa retira o artigo quando não acha conserto. Dan Roberts, líder de pesquisa da OpenAI, anunciou as retiradas no X. Por isso o TechCrunch fala em 719 manuscritos: a conta já desconta os três retirados.
O que os matemáticos cobram?
O Advisory Group on Mathematics and Artificial Intelligence (AGMAI), grupo de nove pesquisadores sediado no Institute for Advanced Study, publicou diretrizes para laboratórios em 29 de setembro. O primeiro pedido foi parar de testar problemas avançados em modelos fechados. O grupo também pediu os prompts, o custo de computação de cada resultado, dados que liguem a prova em texto à prova formal e dinheiro para matemáticos que vão estudar os resultados. A OpenAI usou modelo fechado, não publicou os prompts e deu só a média de computação, segundo o Implicator.ai. A empresa prometeu financiar workshops e conferências.
O AGMAI não deu nota à OpenAI. Disse ao TechCrunch que cabe à comunidade avaliar se as recomendações foram seguidas. A avaliação de que a empresa ficou abaixo do padrão, sobretudo na compreensão humana dos resultados, é do próprio TechCrunch. A Retraction Watch registra outra versão do porta-voz: o grupo teria recomendado publicar sem esperar a formalização completa, e cerca de metade dos resultados saiu sem confirmação.
O número de 42% merece cuidado. O TechCrunch escreveu uma frase ambígua, que pode ser lida como 42% sem formalização. O Implicator.ai deu a conta exata: 300 dos 719 resultados principais tinham prova em Lean em 7 de outubro, cerca de 42%. É essa a leitura que a Marcio.AI adota. Andrew Sutherland, do MIT, disse à Retraction Watch que a reação rápida foi “a coisa responsável a fazer”, mas que muitos matemáticos estão “insatisfeitos” com a OpenAI. Alex Townsend, de Cornell, disse que esperava mais erros e que a empresa deveria ter anunciado primeiro só os artigos verificados em Lean.
Como chegamos até aqui?
O mesmo modelo produziu o resultado sobre as equações de Navier-Stokes que a OpenAI anunciou em 8 de setembro, usando 10 mil agentes e custo de milhões de dólares, segundo o Implicator.ai. O anúncio foi criticado como apressado, e mais de 8 mil pesquisadores endossaram a crítica, segundo a Retraction Watch. Em 29 de setembro o AGMAI publicou as diretrizes. Em 6 de outubro veio a publicação em massa e, no dia seguinte, a retirada.
Um artigo de matemáticos de Cambridge e do King’s College London achou pelo menos duas diferenças entre a prova em texto e o código em Lean do caso Navier-Stokes, segundo o TechCrunch. Os autores dizem que isso não derruba nenhuma das duas provas, mas que elas não devem ser aceitas sem revisão por pares. A IA aplicada à ciência vem ganhando espaço nas últimas semanas, como mostram o AstaBrief do Ai2 e o Quine da Microsoft, já cobertos pela Marcio.AI.
O que isso significa para pesquisa e empresas?
Para centros de pesquisa, inclusive no Brasil, o recado é de método. Prova gerada por máquina tem de chegar com verificação formal ou com revisão humana explícita. Sem isso, o volume vira custo para quem revisa. Para empresas que usam IA em análise técnica, jurídica ou financeira, a lição é a mesma: um erro pequeno no início se espalha para tudo o que depende dele, e a checagem precisa seguir essa cadeia.
O que observar nas próximas semanas
A tese da Marcio.AI: em 2027, publicação científica feita por IA só terá aceitação ampla com prova formal anexada, e a fatia verificada em Lean vira a métrica que importa. A OpenAI ganha visibilidade com o volume e perde confiança a cada retirada.
Sinais para conferir até o fim de 2026: a evolução da fatia de resultados com prova em Lean, novas retiradas ou correções no repositório, a avaliação formal do AGMAI, a liberação do modelo para pesquisadores externos e a publicação dos prompts e do custo por resultado.
Fontes
- OpenAI, Sharing AI progress in mathematics, 06/10/2026
- Exame, OpenAI divulga 722 manuscritos matemáticos criados por IA ainda não lançada, 06/10/2026
- Interesting Engineering, OpenAI largest math release with Lean proofs, 06/10/2026
- Retraction Watch, OpenAI withdraws preprints from 722 manuscripts on unsolved math problems, 08/10/2026
- TechCrunch, OpenAI’s math solutions aren’t meeting the field’s standards yet, 08/10/2026
- Implicator.ai, OpenAI Posts 372 AI Math Results, Then Withdraws Three Papers Over a Sign Error, 08/10/2026
Rating Marcio.AI: 5/5 (Global, Totalmente relevante, No centro do hype). Seção DeepTech do Watcher.
#MarcioAI #OpenAI #Matematica #Lean #PesquisaCientifica #IA
Como este texto foi produzido
Este texto é assinado pelo Marcio.AI, o Gêmeo Digital do portal, que produz a partir de fontes públicas, dentro do recorte editorial definido por Marcio Sampaio N. SANTANA. Ele faz parte do Watcher, a curadoria diária de notícias de tecnologia da Marcio.AI. As fontes estão listadas acima, com veículo e data. A política editorial explica o processo inteiro e como pedir correção de qualquer informação.
Leia também: Ai2 abre o AstaBrief, modelo que escreve relatórios científicos com citações e Microsoft apresenta o Quine, IA de biologia.