OpenAI publica 722 manuscritos; verificação ainda é parcial

Em 6 de outubro de 2026, a OpenAI tornou públicos 722 manuscritos de matemática organizados em 372 famílias, produzidos por um modelo interno ainda não lançado. Os arquivos foram disponibilizados para exame da comunidade matemática. A publicação expõe demonstrações propostas, mas a verificação ainda cobre apenas parte da coleção.

O catálogo público da OpenAI passou a listar 719 manuscritos após as retiradas; cerca de 42% dos resultados principais têm formalização em Lean, e novas formalizações serão acrescentadas ao repositório. A contagem de textos e a cobertura formal medem coisas diferentes: nenhuma delas informa quantos trabalhos receberam revisão por pares ou quantos teoremas serão reconhecidos como contribuições originais.

Como o modelo produziu os manuscritos

A coleção nasceu de avaliações do modelo em problemas de pesquisa em aberto. A maior parte dos resultados seguiu um procedimento comum, e alguns trabalhos partiram de resultados anteriores gerados pelo próprio sistema. O modelo permanece interno; os manuscritos publicados, seus arquivos de apoio e resumos abreviados de parte do raciocínio são os materiais que pesquisadores externos podem examinar.

As famílias organizam trabalhos relacionados, e não problemas necessariamente independentes. Uma família pode conter o resultado principal, argumentos complementares, consequências e demonstrações alternativas. Assim, contar cada manuscrito como uma descoberta separada aumentaria artificialmente o alcance da publicação. Também há dependências entre textos: a correção de um argumento pode afetar outras conclusões construídas sobre ele.

O repositório inclui arquivos dos manuscritos, instruções de citação, um panorama das famílias e materiais ligados às provas. Essa organização permite localizar enunciados e acompanhar versões, mas deixa à comunidade uma tarefa ampla: verificar cada demonstração e situar cada alegação na literatura da especialidade. O volume divulgado, por si só, não informa quais argumentos resistirão a esse exame.

O que o Lean verifica — e o que fica para os matemáticos

Há uma diferença decisiva entre ter uma demonstração escrita e ter uma prova formal checada. No manuscrito, o argumento aparece na linguagem usual da matemática, com etapas que especialistas precisam ler e reconstruir. Em Lean, enunciado e demonstração são representados de modo que o computador confira a validade lógica dos passos para as hipóteses e definições especificadas.

Uma checagem bem-sucedida oferece garantia forte para o enunciado efetivamente formalizado. Seu alcance depende, porém, da correspondência entre essa formulação e a afirmação apresentada no manuscrito: uma versão mais estreita não valida automaticamente todas as consequências anunciadas no texto. Também cabe a matemáticos avaliar se as hipóteses são relevantes e se a conclusão responde ao problema que motivou o trabalho.

Os textos da coleção estão, portanto, em estágios distintos. Um manuscrito público contém uma alegação examinável; uma formalização em Lean permite a checagem computacional de determinado enunciado; a revisão pela comunidade identifica lacunas, dependências e antecedentes. Já a revisão por pares envolve pareceres e uma decisão editorial de um veículo científico. Mesmo depois desses passos, a aceitação de um resultado depende de sua correção e de como ele se encaixa no conhecimento matemático existente.

O erro que reduziu o catálogo

Em 7 de outubro, a Retraction Watch relatou a retirada de três manuscritos por um erro de sinal, que invalidou um argumento e afetou dois trabalhos dependentes, além da revisão de outros 14; um porta-voz da OpenAI disse ao veículo: “We welcome scrutiny and feedback from the mathematical community”. As retiradas mostram uma consequência concreta da relação entre os textos: uma falha localizada pode atingir resultados que usam a mesma construção.

As revisões incluíram reparos de demonstrações, ajustes de enunciados e esclarecimentos sobre hipóteses e dependências. Também houve correção de uma referência desatualizada. As versões anteriores continuam acessíveis, o que permite acompanhar a diferença entre um argumento reparado e um trabalho retirado, sem tratar toda a coleção como se tivesse o mesmo estado de verificação.

A correção pública é parte do exame científico, mas muda o que pode ser afirmado sobre os resultados afetados. Nos textos retirados, a demonstração apresentada deixou de sustentar a alegação original; nos revisados, é a nova versão que precisa ser lida. A extensão de cada alteração importa mais do que a simples existência de uma atualização.

Originalidade ainda depende de exame especializado

Uma prova logicamente correta pode reproduzir uma ideia conhecida, reformular um teorema existente ou depender de contribuição anterior pouco visível na apresentação inicial. Por isso, originalidade exige comparar enunciados, métodos e referências com a literatura da área. A pergunta é diferente daquela respondida por uma checagem formal: Lean pode conferir um encadeamento lógico, mas não decide se o resultado era desconhecido ou importante.

As dúvidas levantadas por matemáticos sobre novidade e dependência de trabalhos anteriores precisam ser avaliadas família por família. A contribuição pode estar no resultado central, em uma técnica de prova ou numa consequência específica; também pode ser menor do que sugere uma apresentação ampla. Esse trabalho se torna mais delicado quando um manuscrito usa outro da mesma coleção como ponto de partida.

O próximo dado concreto virá das formalizações adicionais e do exame das versões corrigidas por especialistas das áreas envolvidas. Esses passos poderão delimitar quais afirmações se sustentam, quais exigem novas correções e onde há uma contribuição matemática realmente nova.