Um mês depois de a OpenAI anunciar uma solução para o problema de Navier-Stokes, um dos sete Problemas do Milênio do Clay Mathematics Institute, três matemáticos publicaram um artigo dizendo que as duas versões da prova divulgadas pela empresa não coincidem. O trabalho, submetido ao arXiv em 6 de outubro de 2026 por Alexander Bastounis, Fabian Circelli e Anders Hansen, foi noticiado pela New Scientist em 8/10.

O que a OpenAI anunciou

Em 8 de setembro, a OpenAI publicou o artigo “Finite time blowup for Navier–Stokes”, assinado pela empresa. Segundo o texto, para qualquer viscosidade positiva existe uma força suave e de suporte compacto que faz uma solução das equações tridimensionais de fluidos incompressíveis partir do repouso e ter velocidade ilimitada em tempo finito, com energia cinética limitada. A empresa diz que isso estabelece as alternativas (C) e (D) do enunciado oficial do problema. O repositório no GitHub, sob licença Apache 2.0, traz formalizações em Lean 4 apresentadas como correspondentes ao artigo e a um segundo trabalho sobre as equações de Euler.

Na cobertura do anúncio, a New Scientist relatou que a OpenAI usou mil agentes de IA por 50 horas no problema de Euler e 10 mil agentes por 11 horas na extensão para Navier-Stokes. Segundo a revista, a empresa estimou em cerca de US$ 15 milhões o custo para um cliente repetir o processo e não revelou o modelo usado. O anúncio veio horas depois de Tristan Buckmaster (NYU) e Levent Alpöge (Anthropic) divulgarem resultados parciais sobre Euler, o que gerou uma disputa pública sobre a origem do trabalho. A OpenAI negou ter usado as provas ou os prompts da dupla. O presidente do Clay Institute, Martin Bridson, disse à revista que a avaliação do prêmio de US$ 1 milhão será “deliberadamente sem pressa”.

Onde está a divergência

Segundo a New Scientist, a divergência está no Lema 8.6. No texto em linguagem natural, um valor precisa ficar abaixo de m + 4; na versão em Lean, o limite é m + 5, uma afirmação matematicamente mais fraca. Os autores atribuem isso à autoformalização: ao converter o texto para Lean, o modelo precisa produzir um código que compile e, ao encontrar um trecho problemático, pode contorná-lo e se afastar do argumento original. A equipe levou cerca de duas semanas para achar a discrepância, usando o ChatGPT para sugerir divergências e conferindo tudo à mão.

Os pesquisadores não afirmam que o problema continua em aberto. “Não estamos dizendo que a prova em linguagem natural está errada. Nem dizemos que está correta”, disse Hansen à revista. Kevin Buzzard, do Imperial College, disse estar confiante de que o problema foi resolvido, mas bem menos confiante de que a prova descrita no PDF esteja correta. Segundo a New Scientist, a OpenAI disse saber da diferença, afirmou que ela não invalida nenhuma das provas e prometeu corrigir erros no texto conforme forem encontrados.

Por que importa

A verificação em Lean garante que o enunciado formal foi provado, não que ele traduz fielmente o texto publicado nem o problema do Clay. Isso pesa porque, segundo a revista, a OpenAI divulgou no início de outubro 722 artigos matemáticos, só parte deles com provas em Lean, que também não foram conferidas à mão. Para o prêmio, o resultado ainda depende da avaliação do Clay Institute, que Bridson promete ser rigorosa.

Fontes

• OpenAI (GitHub) — openai/NavierStokesAndEuler — Lean certificates accompanying Navier-Stokes and Euler results (08/09/2026)
• OpenAI — Finite time blowup for Navier–Stokes (artigo em PDF) (08/09/2026)
• arXiv — Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs (Bastounis, Circelli, Hansen) (06/10/2026)
• New Scientist — OpenAI has solved the Navier-Stokes Millennium problem using $15m of AI effort (08/09/2026)
• New Scientist — OpenAI mistranslated mathematics into code for its Navier-Stokes proof (08/10/2026)

Imagem destacada: ilustração gerada por computador, sem valor documental.