A OpenAI retirou três manuscritos de provas matemáticas produzidas por um modelo interno de inteligência artificial em 7 de outubro de 2026. Um erro de sinal comprometeu um argumento em um texto e uma construção aproveitada em outros dois. Isso não demonstra falha do verificador Lean. O Lean pode confirmar que uma dedução formal segue de hipóteses declaradas, mas essa verificação não garante, sozinha, que o enunciado formal corresponde ao problema matemático pretendido ou que houve uma descoberta inédita.
Da divulgação às correções: o que está documentado
Em 6 de outubro, a OpenAI publicou 722 manuscritos organizados em 372 famílias de resultados no repositório público openai/math. A empresa atribuiu o material a um modelo interno ainda não disponibilizado e apresentou os documentos como resultados de pesquisa em diferentes estágios de verificação. Pré-publicação, nesse contexto, significa um texto divulgado antes da avaliação tradicional por pares, não uma comprovação definitiva.
No registro de 7 de outubro, a empresa retirou três trabalhos, revisou 14 outros manuscritos com reparos e ajustes de hipóteses, enunciados ou referências e atualizou 13 adicionais para citarem versões corrigidas. O mesmo registro contabilizou seis formalizações adicionais e informou 300 resultados principais formalizados em Lean entre 719 manuscritos, aproximadamente 42%. Esse percentual é o cálculo divulgado pela própria OpenAI naquela atualização, não uma auditoria independente de cada arquivo.
O catálogo continuou mudando. Em 26 de outubro, a OpenAI acrescentou dois manuscritos acompanhados de formalizações; o README consultado em 30 de outubro passou a informar 721 manuscritos em 373 famílias. Em 29 de outubro, o histórico registrou uma correção de nomes de espaços no desafio e na solução do Comparator de outro resultado, sobre variedades abelianas CM. Essa alteração não deve ser confundida com a retirada de 7 de outubro nem com o trabalho retirado sobre produtos de superfícies K3.
Quais foram os três trabalhos retirados?
O registro oficial identifica os manuscritos pelos seguintes títulos originais:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
O primeiro manuscrito continha um erro de sinal que invalidava um argumento de cancelamento ligado a traços de estabilização. Dois textos seguintes dependiam da construção afetada. Por isso, os três foram retirados; os registros preservam avisos sobre a lacuna e apontam para as versões arquivadas. É uma falha na argumentação apresentada, não uma demonstração de que as conjecturas sejam falsas.
O que o Lean verifica de verdade?
Lean é uma linguagem e um assistente de demonstração formal. Em vez de aceitar uma explicação em linguagem natural por parecer convincente, seu núcleo verificador confere se um objeto de prova sustenta uma proposição escrita com definições e regras lógicas precisas. A documentação distingue a busca de uma prova de sua checagem: um sistema de IA pode sugerir o raciocínio, enquanto o verificador avalia a representação formal apresentada.
A garantia é condicionada ao enunciado formal, às definições, aos axiomas e às dependências utilizados. Um teorema pode estar perfeitamente demonstrado no Lean e ainda tratar de uma versão mais restrita, diferente ou inadequadamente traduzida da afirmação matemática em linguagem comum. Por exemplo, provar uma propriedade para uma classe especial de objetos não equivale a prová-la para todos os objetos, mesmo se a prova formal estiver correta.
O manual do Lean alerta que uma marca visual de aprovação não basta para todas as auditorias: dependências podem conter sorry, um marcador de prova incompleta que se torna um axioma. O comando #print axioms ajuda a inspecionar as hipóteses e axiomas usados, incluindo dependências indiretas. Em verificações mais exigentes, lean4checker e comparator permitem novas checagens; o Comparator compara o teorema demonstrado com um enunciado de desafio preparado em ambiente confiável. Mesmo esse procedimento depende da correção do desafio e das definições.
Três perguntas que não podem ser misturadas
| Etapa | O que é examinado | Limite decisivo |
|---|---|---|
| Validade lógica | A prova formal decorre das definições, axiomas e premissas declaradas? | Checagem técnica não corrige automaticamente um enunciado mal formulado. |
| Correspondência do enunciado | A proposição codificada traduz a conjectura original, sem enfraquecê-la? | Exige análise matemática do significado das definições e hipóteses. |
| Contribuição científica | O resultado é novo, relevante, inteligível, atribuível e sustentado pela comunidade? | Requer exame da literatura, crítica independente e discussão científica; não decorre apenas de compilar código. |
O contraponto dos matemáticos e a origem das ressalvas
Em reportagem de 8 de outubro, a Retraction Watch registrou que, segundo um porta-voz da OpenAI, a falha foi identificada numa auditoria da própria empresa. O matemático Alex Townsend, da Universidade Cornell, defendeu que os trabalhos já formalizados deveriam ter sido divulgados separadamente dos demais. Andrew Sutherland, do MIT, considerou adequada a retirada rápida, mas ressaltou que recuperar confiança exigiria mais trabalho. São avaliações atribuídas a esses pesquisadores, não um parecer universal da comunidade.
Em recomendações publicadas em 29 de setembro de 2026, o grupo consultivo independente AGMAI pediu clareza sobre qual modelo produziu os resultados, instruções, tentativas, custo computacional, formalizações e identificação explícita dos trabalhos ainda não verificados. Também enfatizou a compreensão humana, a revisão por pares quando pertinente e a preservação do registro das correções. Seu conselho permite divulgar material ainda sem plena formalização sob condições de transparência; não transforma essa divulgação em validação científica.
Em 26 de outubro, a própria OpenAI passou a descrever os materiais de IA como dados brutos de pesquisa e anunciou formatos diferentes de colaboração com especialistas para explicar novos resultados. Essa evolução de procedimento não revalida retroativamente os três manuscritos retirados.
O que o episódio permite concluir
A conclusão documentada é delimitada: três argumentos publicados não se sustentaram na forma divulgada, e a OpenAI corrigiu ou atualizou outros textos. Isso não autoriza afirmar que todo o catálogo é inválido, que o Lean aprovou aquelas três demonstrações ou que houve defeito no núcleo do verificador. Os documentos consultados não apresentam execução independente, pelo DTech, das formalizações nem uma checagem completa de todos os manuscritos.
Para interpretar qualquer nova prova de IA, é preciso identificar qual enunciado foi realmente formalizado, se as dependências e axiomas foram auditados, que fração do argumento foi conferida, quem examinou a correspondência com a conjectura e que revisão científica ocorreu. O selo de uma checagem lógica responde a uma pergunta importante, mas não substitui as outras.
Fontes e referências
- OpenAI, anúncio de 6 de outubro
- OpenAI, repositório e estado do catálogo
- OpenAI, histórico de retiradas e correções
- Lean, manual de validação formal
- Lean, introdução à demonstração de teoremas
- Retraction Watch, apuração independente de 8 de outubro
- AGMAI, recomendações de 29 de setembro
- OpenAI, proposta de colaboração com pesquisadores de 26 de outubro
