A OpenAI colocou no ar um corpus de 722 manuscritos de pesquisa matemática no repositório openai/math (abre em nova aba). No dia seguinte à divulgação, o primeiro registro de mudanças (abre em nova aba) do projeto, datado de 7 de outubro de 2026, comunicou a retirada de três deles.
O motivo coube em uma linha.
Um sinal trocado. A escala de produção era inédita; o modo de falha, o mais antigo da matemática.
O que o registro diz, exatamente
Segundo a OpenAI, um erro de sinal no manuscrito Algebraicity of Weil classes on split abelian eightfolds invalida um argumento de cancelamento por traço de estabilização e a construção usada por dois artigos dependentes. Em consequência, três manuscritos foram retirados:
| Manuscrito retirado | Papel na cadeia |
|---|---|
| Algebraicity of Weil classes on split abelian eightfolds | Origem do erro |
| Algebraicity of Kuga–Satake Correspondences for K3 Surfaces | Depende da construção invalidada |
| The rational Hodge conjecture for products of K3 surfaces | Depende da construção invalidada |
A cobertura do episódio acrescenta os números que cercam a decisão: o repositório passou de 722 para 719 manuscritos, e os três textos retirados agora carregam avisos que explicam a lacuna e apontam para as versões arquivadas. Ou seja, os artigos não desapareceram; foram marcados como inválidos, com trilha de auditoria preservada.
No mesmo registro, a OpenAI relata ter revisado outros 14 manuscritos, com consertos de demonstração, enunciados corrigidos, hipóteses e dependências mais claras e um ajuste de citação obsoleta. Outros 13 manuscritos tiveram apenas as referências atualizadas para citar as edições revisadas dos textos companheiros. Um commit de 8 de outubro, assinado "Update manuscripts and Lean formalizations", consolida o conjunto.
Anatomia de um sinal
Vale entender que tipo de argumento morreu, porque nem todo erro de sinal derruba uma demonstração. Alguns derrubam.
Em matemática, argumentos de cancelamento são onipresentes: conta-se objetos com sinais associados, mostra que os termos aparecem em pares cujas contribuições se somam a zero e, com isso, elimina-se da conta tudo o que seria incômodo carregar até o fim. A validade do cancelamento costuma depender de sinais derivados de convenções de orientação e de consistência interna do formalismo. É nesse ponto que o manuscrito falhou.
Segundo a explicação registrada e os detalhes reportados pela imprenda especializada, o artigo anotou com sinal +1 uma classe de operações geométricas que, pela convenção do próprio texto, deveria receber -1. Uma troca aparentemente cosmética. Com o sinal errado, os termos que deveriam se cancelar até zero deixam um resto diferente de zero, e um teorema clássico invocado na demonstração exige exatamente que essa contagem seja nula. A premissa deixa de valer no ponto em que era mais necessária.
Um sinal. Só isso.
Para um público de engenharia, a analogia é imediata: é o equivalente a um sinal invertido em uma diferença finita, onde o cancelamento das parcelas de erro sustenta a estabilidade do método inteiro. A diferença é que em análise numérica o erro costuma aparecer no resultado; em uma demonstração, ele fica invisível até que alguém retrace o argumento com atenção obsessiva às convenções.
Hodge, K3 e a corrente que rompeu
Os três manuscritos retirados pertencem, segundo a cobertura, ao território da conjectura de Hodge, um dos sete problemas do milênio do Clay Mathematics Institute (abre em nova aba), com prêmio de um milhão de dólares para quem resolvê-la. Em linhas gerais, a conjectura pergunta quais classes de cohomologia com coeficientes racionais de uma variedade algébrica vêm de subvariedades, ou seja, de ciclos algébricos genuínos.
As três peças cobriam classes de Weil em variedades abelianas split de dimensão oito, correspondências de Kuga–Satake, aquela construção clássica que conecta as estruturas de Hodge de superfícies K3 a variedades abelianas, e o caso racional da conjectura para produtos de superfícies K3. Títulos técnicos para um programa técnico: aproximar a conjectura por casos especiais em que as ferramentas disponíveis alcançam.
Aqui está o ponto estrutural do episódio. O segundo e o terceiro manuscritos não contêm, pelo que se sabe, erros próprios. Caíram porque a construção do primeiro é insumo deles. Em uma cadeia de dependências matemáticas, um único pilar comprometido derruba tudo o que está apoiado nele, e é razoável inferir que a OpenAI optou por retirar os dois textos dependentes de forma preventiva, já que seus argumentos herdam a lacuna. O registro, aliás, descreve exatamente isso: o erro invalida a construção usada por dois artigos dependentes.
Essa é a natureza da matemática como disciplina encadeada. Não é o edifício inteiro que desaba, é a viga de carga, e tudo montado sobre ela desce junto.
O que sobrou de pé
O registro de 7 de outubro não é só a lista do que caiu. É também o mapa do que resistiu e do que foi consertado.
As 14 revisões incluem consertos reais de demonstração, não apenas ajustes editoriais: enunciados corrigidos, hipóteses explícitas, dependências declaradas. Para um corpus dessa escala, publicado há menos de dois dias, passar por essa triagem tão rápido diz algo sobre o processo interno de verificação, ainda que o registro não detalhe como as revisões foram identificadas nem quem as encontrou. Fato: houve triagem e houve retratação. Inferência possível: o processo de revisão estava planejado antes mesmo da divulgação.
O item mais revelador para quem trabalha com verificação formal está no fim do registro. A OpenAI acrescentou seis formalizações novas e cinco adições de suporte, elevando o total de resultados principais formalizados para 300 de 719, cerca de 42%. A referência é ao Lean (abre em nova aba), o assistente de provas cujo núcleo reduzido verifica demonstração linha a linha, sem depender de convenção humana lembrada corretamente.
A ironia é factual, não retórica. Um erro de sinal é precisamente a classe de defeito que um assistente de provas elimina por construção: o kernel não aceita o passo se as convenções não baterem. O que o episódio expõe é a fronteira atual: 42% dos resultados de ponta formalizados significa que a maioria ainda vive no regime antigo, em que o olho humano é o verificador de último recurso, e nesse regime o +1 no lugar de -1 atravessa.
O registro não informa se os três manuscritos retirados tinham alguma porção formalizada, e seria especulação afirmar. O que se pode dizer é o que os números permitem: a cobertura formal ainda é parcial, e o custo dessa parcialidade acabou de ficar visível.
Retração tratada como engenharia de software
A reação que importa aqui não é a de fóruns, mas a do próprio formato. A gente se acostumou, em matemática, a errata em letra miúda, circulação de cartas informais sobre "aquele artigo com problema" e citações que continuam acontecendo por anos depois da descoberta de uma lacuna. Retratação formal, na cultura matemática tradicional, é rara; o mecanismo padrão é o conserto publicado ou, na pior das hipóteses, o silêncio.
O que a OpenAI fez foi outra coisa. Registrou a retirada em um changelog, versionou os manuscritos, manteve as edições antigas acessíveis, propagou a correção pelas citações dependentes e marcou os textos problemáticos com avisos rastreáveis. É o modelo de manutenção de software aplicado à pesquisa: transparência como processo, não como gesto.
Há leitura crítica a fazer. Um erro dessa natureza ter chegado à publicação indica que a revisão que precedeu a divulgação do corpus tinha limites, e o próprio registro admite isso implicitamente ao listar os consertos. Dizer que o sistema funcionou porque a retratação foi rápida e honesta, e dizer que falhou porque o sinal atravessou, são as duas frases verdadeiras, e é honesto sustentá-las juntas. Sobre planos futuros, o registro é lacônico: menciona avisos e versões arquivadas, mas não anuncia republicação, correção do artigo raiz nem investigação interna. Qualquer afirmação nessas direções, hoje, seria leitura de silêncio.
O que fica sustentado pelas evidências é um contraste instrutivo: 722 manuscritos produzidos e divulgados em escala, três derrubados por um sinal, e um subconjunto crescente verificado por máquina. O número que melhor resume o estado das coisas não é o 722 nem o 3. É o 300: os resultados principais que um kernel formal já consegue conferir sozinho, contra os 419 que ainda dependem de convenções lidas com atenção por olhos humanos.