O que a OpenAI colocou online
A OpenAI publicou o material que sustenta a sua alegação de ter encontrado uma singularidade em tempo finito nas equações de Navier-Stokes a três dimensões: um relatório no seu próprio site, um artigo e ficheiros de prova verificáveis por máquina num repositório público do GitHub. A empresa diz que não tenciona reclamar o prémio de um milhão de dólares do Clay Mathematics Institute.
É essa a mudança face a segunda-feira, quando a alegação existia apenas como uma descrição que circulava entre investigadores. O repositório contém formalizações em Lean 4, construídas sobre a Mathlib e publicadas sob licença Apache 2.0, para dois casos de Navier-Stokes com viscosidade positiva — um no espaço inteiro e outro no toro periódico — e para uma construção de Euler associada. Quem tiver o Lean instalado pode agora correr o certificado em vez de aceitar a alegação por confiança.
Os números que a OpenAI apresenta
Os dados de computação vêm da OpenAI e não foram auditados de forma independente. A empresa diz que o trabalho usou um modelo interno que descreve como bastante mais capaz do que o GPT-6 Astra, e que cerca de 10 000 agentes correram em paralelo durante aproximadamente 88 horas no início de setembro, produzindo na ordem dos 130 mil milhões de tokens de saída. Outras 17 horas, segundo o The Next Web, foram gastas a formalizar o argumento com o GPT-6 Astra.
Isso são recursos, não provas. A prova é o ficheiro Lean, e o Lean não se importa com quantos agentes o escreveram.
Porque não reclama o prémio
A formulação de Clay para o problema de Navier-Stokes divide-se em quatro enunciados. A OpenAI diz que o seu resultado estabelece os enunciados C e D: as alternativas de rutura, que resolvem o problema exibindo uma solução que deixa de ser suave. E diz também que não vai reclamar o prémio.
A razão está na construção. O fluido parte do repouso e é-lhe aplicada uma força externa suave durante todo o processo, e a singularidade desenvolve-se sob essa força. Se um exemplo forçado conta para a pergunta clássica é um juízo que cabe aos matemáticos e a Clay, não a um assistente de prova. A página do instituto continua a listar Navier-Stokes como problema em aberto.
A disputa pelo crédito continua
O resultado chega no meio de uma discussão que o Aivio News contou na segunda-feira. Tristan Buckmaster, da Universidade de Nova Iorque, e Levent Alpöge, da Anthropic, publicaram as suas próprias provas de explosão assistidas por IA e verificadas em Lean para as equações do meio poroso, de Boussinesq e de Euler, e Buckmaster divulgou uma declaração a descrever como a OpenAI o abordou sobre o calendário e a autoria do resultado de Navier-Stokes. Sébastien Bubeck, da OpenAI, classificou esse relato como falso e incendiário.
A Quanta Magazine noticiou que Charles Fefferman, de Princeton, autor do enunciado oficial do problema, chamou a Diego Córdoba e Luis Martínez-Zoroa os heróis desta história: a dupla cujo método não computacional serve de base a ambos os esforços.
O que vigiar
Duas coisas passam agora a ser verificáveis em vez de discutíveis. A primeira é se matemáticos independentes compilam os ficheiros Lean e confirmam que provam o que o relatório diz. A segunda é se o Clay Mathematics Institute se pronuncia sobre os termos de forçamento. Até lá, a descrição honesta é que existe uma singularidade verificada por máquina e que a sua relação com a pergunta do prémio está por decidir.
