Navier–Stokes e a prova em Lean: singularidades forçadas e opacidade de laboratório

Em 8 de setembro de 2026 a OpenAI declarou que um modelo interno seu, nunca distribuído ao público, produziu uma demonstração de blowup em tempo finito para as equações de Navier–Stokes tridimensionais incompressíveis. A empresa divulgou o documento teórico e o repositório público NavierStokesAndEuler, que contém a formalização na linguagem Lean 4 dos teoremas relativos a dados iniciais regulares submetidos a um termo de forçamento externo. Segundo a reconstrução do laboratório, o resultado cobre os enunciados de quebra de regularidade da formulação redigida pelo matemático Charles Fefferman para o Clay Mathematics Institute, sem contudo enfrentar o caso sem força externa, considerado pela comunidade científica a variante mais difícil do problema. O autor da formulação oficial classificou a resolução como entusiasmante, citando as contribuições de Córdoba e Martínez-Zoroa, ao passo que a empresa esclareceu desde o início que não pretende reivindicar o prêmio de um milhão de dólares.

A operação entrelaça a automação matemática com os tempos das instituições acadêmicas. O Clay Mathematics Institute continua a listar Navier–Stokes entre os problemas não resolvidos: o regulamento exige publicação em veículo qualificado, uma espera de pelo menos dois anos após a publicação e a aceitação geral pela comunidade matemática, sem que o instituto tenha até agora se manifestado quanto ao mérito. Seu presidente, Martin Bridson, lembrou que a avaliação segue de propósito um ritmo sem pressa, para garantir rigor absoluto. O quadro fica mais intrincado com uma controvérsia de prioridade envolvendo um trabalho paralelo apresentado pelo matemático Terence Tao e descrito pelos autores como fortemente assistido por inteligência artificial. Um matemático da Universidade de Nova York contestou a reconstrução dos contatos fornecida pelo laboratório, levantando a hipótese de que sessões privadas com uma ferramenta proprietária possam ter contribuído para o resultado; a empresa negou ter visto diretamente o trabalho não publicado, admitindo porém não poder excluir o impacto de dados de uso desidentificados no treinamento dos próprios modelos.

O repositório indica as instruções para que a demonstração seja reconferida por máquina, mas até agora nenhuma verificação independente foi concluída; para além desse controle, a natureza proprietária da infraestrutura empregada impede qualquer verificação independente sobre os custos e as métricas de eficiência exibidas. O cálculo declarado — cerca de dez mil agentes concorrentes entre 1º e 5 de setembro, com 88 horas até chegar à demonstração e outras 17 para a formalização e a verificação em Lean — permanece confinado a afirmações corporativas que ninguém consegue reproduzir de fora. Sem acesso ao código de treinamento nem aos pesos do sistema, a comunidade científica só pode validar os passos formais depositados no repositório, deixando na sombra as condições reais de reprodutibilidade do experimento.

A matemática formal encontra um aliado formidável na conferência automática dos passos lógicos, mas a corrida pela primazia científica por meio de modelos fechados mostra seus limites estruturais. Verificar um teorema já é tarefa executável por uma máquina; estabelecer a transparência da cadeia que o gerou ainda exige um rigor inteiramente humano.

— Olya