722 Manuscritos em Um Dia: O Que Poderia Dar Errado?

No dia 6 de outubro de 2026, a OpenAI despejou 722 preprints matemáticos em um repositório no GitHub. Eram trabalhos sobre 372 problemas abertos de geometria, álgebra, ciência da computação e teoria dos conjuntos. O anúncio veio com o tom habitual: a IA está resolvendo problemas que humanos não conseguiram resolver em décadas.

Menos de 24 horas depois, a OpenAI retirou 3 manuscritos e corrigiu outros 14.

O erro? Um sinal trocado. Literalmente +1 onde deveria ser -1. Um erro que qualquer estudante de graduação pegaria numa revisão de pares. E que invalidou não apenas o paper original, mas dois outros que dependiam dele.

A Associação pela Matemática Humana não perdoou: “Liberar mais de 700 arquivos de uma vez não é uma demonstração de conhecimento, é uma demonstração de poder.”

O Que a OpenAI Estava Tentando Provar

A OpenAI vem investindo pesado em matemática com IA. A ideia é usar modelos de linguagem (e verificadores formais como o Lean) para atacar problemas abertos da matemática. Em setembro, já tinham causado polêmica ao anunciar resultados sobre as equações de Navier-Stokes, atraindo mais de 8.000 pesquisadores que assinaram uma carta expressando preocupação com o ritmo apressado das publicações.

O drop de outubro foi ainda mais ambicioso. Entre os 722 manuscritos, havia trabalhos sobre conjectura de Hodge, teoria dos conjuntos, geometria algébrica e outros problemas que os melhores matemáticos do mundo vêm trabalhando há gerações.

O resultado mais chamativo: uma suposta prova de que o Princípio da Partição não implica o Axioma da Escolha. Para quem não é de teoria dos conjuntos, esse é um problema aberto há mais de um século. Resolver isso seria equivalente a encontrar o Santo Graal da lógica matemática.

O Erro do Sinal: +1 Onde Deveria Ser -1

Dos três papers retirados, todos estavam relacionados à conjectura de Hodge. O erro central era absurdamente simples: em um argumento chave, o primeiro paper usou +1 como símbolo para uma operação geométrica que deveria ser -1.

Esse erro de sinal invalidou o que a OpenAI chamou de “stabilization-trace cancellation argument”. E como dois outros manuscritos usavam essa construção como base, o efeito cascata derrubou todos os três.

Paper 1: "Algebraicity of Kuga-Satake Correspondences for K3 Surfaces"
  → Erro: sinal trocado no argumento de cancelamento
  → Status: RETIRADO

Paper 2: Dependia da construção do Paper 1
  → Status: RETIRADO (por dependência)

Paper 3: "The rational Hodge conjecture for products of K3 surfaces"
  → Também dependia do Paper 1
  → Status: RETIRADO (por dependência)

Outros 14 manuscripts: corrigidos com "proof repairs, corrected
statements, clearer hypotheses"

Andrew Sutherland, do MIT, chamou a retirada rápida de “a coisa responsável a se fazer”. Ele tem razão, retratar rápido é melhor do que insistir no erro. Mas a pergunta que ninguém quer fazer é: se o erro era tão elementar, por que não foi pego antes de publicar?

O Problema da Verificação Formal (Ou a Falta Dela)

Aqui é onde a coisa fica interessante de verdade. A OpenAI tinha verificação formal em Lean para aproximadamente 42% dos resultados. Os outros 58%? Foram publicados sem verificação formal, apenas com a revisão do modelo de IA.

O comitê consultivo da OpenAI (Advisory Group on Mathematics and Artificial Intelligence) recomendou liberar os resultados “sem aguardar a formalização completa”. A justificativa era que a comunidade matemática poderia ajudar a verificar. Na prática, isso significa que a OpenAI tratou a comunidade matemática como QA gratuito.

Alex Townsend, de Cornell, não gostou. Segundo ele, a OpenAI deveria ter anunciado primeiro os manuscritos que tinham prova verificada em Lean e pedido ajuda da comunidade para os outros. Em vez disso, largaram tudo de uma vez e criaram uma situação onde ninguém sabe o que é confiável e o que não é.

Para quem trabalha com software, a analogia é perfeita: imagine fazer deploy de 722 features em produção, onde 58% não passaram em nenhum teste automatizado, e depois dizer “a comunidade vai testar pra gente”. É o “move fast and break things” aplicado à matemática pura.

O Princípio da Partição: Um Século de Tentativas

O resultado mais polêmico do drop foi a suposta prova sobre o Princípio da Partição e o Axioma da Escolha.

Para simplificar brutalmente: o Axioma da Escolha é um dos pilares da matemática moderna. Ele diz que, dado qualquer coleção de conjuntos não-vazios, é possível escolher um elemento de cada um. Parece óbvio, mas as consequências são profundas e às vezes contraintuitivas (como o paradoxo de Banach-Tarski, que permite “duplicar” uma esfera).

O Princípio da Partição é uma afirmação mais fraca que diz, essencialmente, que se um conjunto A pode ser particionado em partes que correspondem a elementos de B, então existe uma função de A para B. A questão de um século: o Princípio da Partição implica o Axioma da Escolha? A OpenAI afirmou que não.

Asaf Karagila, um dos principais pesquisadores em teoria dos conjuntos do mundo, analisou o manuscrito. Seu veredicto foi devastador.

O paper era “confuso, embolado, com uma estrutura estranha”. A terminologia estava “um pouco fora”, os teoremas e lemas tinham uma organização inesperada, e as citações usavam “três notas de aula não publicadas, não revisadas, e fora do arXiv” como referência. Karagila foi direto: “se isso fosse um paper acadêmico submetido a um periódico, deveria receber uma rejeição de mesa pela qualidade”.

Ele também apontou que era impossível entender a estratégia da prova por leitura superficial, algo raro em papers de teoria dos conjuntos, onde a estrutura argumentativa costuma ser clara mesmo quando os detalhes são densos.

“Negação de Serviço” Contra a Matemática

A crítica mais afiada de Karagila não era sobre os erros em si. Era sobre o formato.

Ele comparou o drop de 722 manuscritos a um ataque de negação de serviço (DoS) contra a comunidade matemática. A ideia é simples: se você despeja centenas de papers de qualidade questionável de uma vez, consome a capacidade limitada de revisão da comunidade. Os matemáticos não têm tempo de revisar 722 manuscritos. Eles mal têm tempo de revisar os papers que já existem no pipeline.

E o resultado político é perverso. Financiadores e formuladores de políticas públicas veem os números (“722 manuscritos! 372 problemas resolvidos!”) e concluem que a IA está substituindo matemáticos. Isso ameaça financiamento de pesquisa básica, posições acadêmicas e a própria estrutura do trabalho matemático.

Nas palavras de Karagila: “parece que as empresas de IA gostariam que nos conformássemos aos padrões delas”, em vez de seguir as normas de comunicação científica que existem por boas razões.

O Que uma Prova em Lean Realmente Verifica

Para devs que usam Lean ou ouviram falar dele, uma nuance importante: uma prova verificada em Lean confirma que a cadeia lógica do argumento é válida, dada as definições e axiomas fornecidos. Mas não verifica se as definições correspondem ao que o paper afirma estar provando.

Em termos de software: o Lean verifica que o código compila e passa nos testes unitários. Mas se os testes estão testando a coisa errada, o Lean não vai pegar isso.

-- Exemplo simplificado do gap

-- O paper AFIRMA provar que P implica Q
-- O Lean VERIFICA que, dado os axiomas A1, A2, A3, a conclusão segue

-- MAS: os axiomas A1, A2, A3 realmente capturam P?
-- E a conclusão realmente representa Q?
-- Lean não responde isso.

Isso é o que os matemáticos chamam de “gap de fidelidade”: a distância entre o que o paper afirma em linguagem natural e o que a formalização em Lean realmente verifica. E esse gap pode ser enorme.

A OpenAI tinha ~42% dos resultados formalizados em Lean. Mas mesmo esses 42% só são confiáveis na medida em que a formalização captura fielmente o problema original. Sem revisão humana dessa correspondência, a verificação formal é necessária mas não suficiente.

Lições para a Indústria de IA

Esse episódio expõe um problema estrutural na forma como a IA é aplicada em pesquisa.

Quantidade não é qualidade. A OpenAI priorizou volume (722 manuscritos de uma vez) em vez de rigor (verificação completa antes da publicação). O resultado foi previsível: erros elementares em papers de alto impacto. Se você é gestor de produto, essa história deveria te assustar. Quantidade de output sem controle de qualidade é dívida técnica com juros compostos.

O modelo não substitui a revisão humana. Os 58% de resultados sem verificação formal foram publicados porque o modelo “achava” que estavam corretos. Isso é o equivalente a confiar em code review automatizado sem nunca ter um humano olhando o diff. Funciona para catch trivial, falha para erros sutis.

Lean é CI/CD, não deployment. A verificação formal é uma ferramenta de validação, não a palavra final. Assim como testes automatizados pegam regressões mas não garantem que o produto resolve o problema certo, Lean verifica lógica formal mas não garante que o teorema formalizado corresponde ao teorema que você queria provar.

A comunidade não é QA gratuito. Esperar que a comunidade matemática verifique 722 manuscritos é tão razoável quanto fazer um release de 722 features e esperar que seus usuários façam o testing. Possível? Sim. Profissional? Não.

O Que Mudou Desde Navier-Stokes

Esse não é o primeiro tropeço da OpenAI em matemática. Em setembro, o anúncio sobre as equações de Navier-Stokes gerou uma reação forte, com mais de 8.000 pesquisadores assinando uma carta de preocupação.

A diferença agora é a escala. Navier-Stokes foi um único resultado controverso. O drop de outubro foram 722 manuscritos, dos quais 3 foram retirados e 14 corrigidos em menos de 48 horas. E o Princípio da Partição, o resultado mais ambicioso, recebeu críticas devastadoras sobre qualidade editorial.

A OpenAI respondeu com diplomacia: “acolhemos escrutínio e feedback da comunidade matemática” e se comprometeu a “corrigir prontamente erros identificados ou retirar papers que não podem ser consertados”.

A comunidade matemática respondeu com ceticismo. Porque corrigir rápido é bom, mas não precisar corrigir seria melhor.

O Paralelo com Software: Já Vimos Esse Filme

Se você é dev, essa história toda soa familiar. É o mesmo padrão que vemos quando empresas priorizam velocidade de entrega sobre qualidade.

Pensa no ciclo: a pressão por resultados leva a cortar corners na verificação. Os erros aparecem em produção. A equipe corre para corrigir. A empresa faz um postmortem, promete melhorar processos, e três meses depois repete o ciclo.

A OpenAI fez exatamente isso. Em setembro, o resultado de Navier-Stokes gerou backlash. Em outubro, a resposta foi… publicar 722 manuscritos de uma vez, com metade sem verificação formal. Isso não é aprendizado, é escalação.

A diferença é que bugs em software podem ser corrigidos com um hotfix. Erros em matemática publicada contaminam a literatura. Outros pesquisadores citam resultados incorretos, constroem trabalho em cima deles, e anos depois alguém descobre que o fundamento estava errado. O custo de um “bug” matemático se propaga por gerações.

Uma tabela para colocar as coisas em perspectiva:

A coluna da direita deveria deixar qualquer engenheiro desconfortável. Publicar com 42% de cobertura de testes não passa em nenhuma code review séria. Mas quando é IA fazendo matemática, de repente vira “demonstração de progresso”.

O Futuro da Matemática Assistida por IA

Apesar de todo o drama, seria desonesto dizer que IA em matemática é puro hype. Os ~42% de resultados com verificação formal em Lean são potencialmente contribuições reais. Mesmo o paper do Princípio da Partição, se revisado e corrigido, pode conter ideias válidas dentro da estrutura confusa.

O problema não é a IA fazendo matemática. É a IA fazendo matemática sem supervisão adequada e publicando em massa sem curadoria. É tratar a pesquisa matemática como um pipeline de conteúdo onde quantidade de output é a métrica principal.

Terry Tao, provavelmente o matemático vivo mais respeitado do mundo, publicou um ensaio na mesma semana perguntando “O que devemos dizer aos nossos alunos?” sobre o impacto da IA na matemática. A pergunta não é retórica. A geração de estudantes que está entrando na graduação agora precisa decidir se vale a pena dedicar uma carreira a provar teoremas quando uma IA pode gerar 722 manuscritos em um dia.

A resposta, pelo menos por enquanto, está nos detalhes. A IA gera 722 manuscritos. Três estão errados. Quatorze precisam de correções. E os que restam precisam de humanos para confirmar que realmente provam o que afirmam provar.

Então talvez a pergunta certa não seja “a IA vai substituir matemáticos?” e sim “quantos matemáticos vão ser necessários para verificar tudo que a IA produz?”

Porque se esse ritmo continuar, a resposta é: mais do que temos hoje.

Fonte de inspiração: OpenAI, the Partition Principle, and Mathematics | Retraction Watch