OpenAI retira artigos matemáticos e abre debate sobre provas formais

Premissas frágeis desafiam provas em Lean

A verificação formal não garante que a formulação matemática inicial esteja correta. Para obter o catálogo, a OpenAI submeteu cerca de 4.000 problemas a um modelo interno não lançado comercialmente, gastando uma média de três horas de processamento no ChatGPT Pro para cada resultado. A empresa publicou resultados de aproximadamente 700 desses 4.000 problemas antes das correções no arquivo history.md. No Hacker News, a atualização gerou 577 comentários e acumulou 322 pontos entre engenheiros e pesquisadores. A comunidade técnica concentrou as críticas nas falhas de premissa que passam batidas por verificadores sintáticos.

O usuário Thorentis comparou o processo a um erro comum de engenharia de software ao avaliar as provas aprovadas: "Como sabemos se as premissas das provas 'verificadas' em Lean estão corretas? Quanto mais penso nesses resultados, mais me convenço de que isso é como um engenheiro júnior que escreve 100 testes unitários e compartilha uma captura de tela do Pytest todo verde, mas você checa o código e a maioria só faz assert True." O comentário resume a desconfiança de quem programa rotinas de teste. O verificador aceita a dedução se a premissa estiver vazia.

Outros participantes levantaram a hipótese de alucinação pura durante as etapas intermediárias de cálculo. O usuário MisterMunchkin criticou a consistência lógica do processo: "Então é tudo apenas lixo alucinado. O modelo simplesmente alucina uma resposta e depois inventa os passos para acompanhá-la! Exatamente como quando eles começam a trapacear e mentir porque o problema é impossível." Provas longas mascaram passos falsos. Essa fragilidade estrutural irrita matemáticos e cientistas da computação.

Engenharia de software entra na matemática pura

A disciplina de desenvolvimento agora dita o ritmo de correção de provas acadêmicas. O usuário renyicircle destacou como a dinâmica de controle de versão alterou a produção científica tradicional: "É assim que fica quando práticas de engenharia de software encontram a matemática. 'openai/math release 1.3.42: artigos 139 e 140 retratados, corrigido um erro de sinal no artigo 47, restaurado o artigo 85 anteriormente retratado, refatorados os argumentos no artigo 101'." Os pesquisadores da OpenAI recolheram três textos específicos: Algebraicity of Weil classes on split abelian eightfolds, Algebraicity of Kuga–Satake Correspondences for K3 Surfaces e The rational Hodge conjecture for products of K3 surfaces. O versionamento expõe o processo em público.

Os dois lados concordam que aplicar três horas de processamento por resultado em milhares de problemas gera dados valiosos sobre os limites reais de modelos de linguagem. Quem constrói sistemas automatizados concorda também que a inspeção humana ainda dita a validade de qualquer premissa submetida ao Lean. O debate deixa em aberto se a OpenAI retirou os artigos por alerta de matemáticos externos ou por checagens feitas por outros modelos executados em lote. Para quem decide arquitetura e adota modelos de raciocínio em produção, o episódio prova que testes automatizados só protegem o código quando a especificação de entrada não contém armadilhas lógicas.