Anúncio de setembro de 2026 propõe um avanço em um dos Problemas do Milênio. Pesquisadores apontam diferenças entre a prova escrita e sua formalização computacional.
Por Graziela Stratotti de Almeida
Em 8 de setembro de 2026, a OpenAI anunciou uma solução para o problema de existência e suavidade de Navier–Stokes. A empresa apresentou uma demonstração matemática e uma versão formalizada em Lean, sistema utilizado para verificar argumentos por computador. O resultado anunciado permanece sujeito à validação independente.
A relevância da notícia exige atenção à revisão científica. Em 27 de outubro, o King’s College London divulgou uma análise de pesquisadores da instituição e da Universidade de Cambridge sobre divergências entre as duas versões da prova.
Imagem de destaque: vórtices de von Kármán nas Ilhas Aleutas, 4 de julho de 2002. Crédito: USGS/EROS Center, Landsat 7. Domínio público. Imagem ilustrativa de escoamento atmosférico.
A pergunta por trás das equações de Navier–Stokes
As equações de Navier–Stokes descrevem a evolução da velocidade e da pressão de fluidos. Na formulação estudada, o fluido é incompressível e possui viscosidade positiva. A dificuldade central envolve saber em quais condições um movimento inicialmente suave pode continuar regular ao longo do tempo.
A formulação oficial de Charles Fefferman, publicada pelo Clay Mathematics Institute, admite quatro alternativas. Duas tratam da existência de soluções suaves sem força externa; outras duas admitem demonstrar uma ruptura da regularidade com uma força suave, sob condições específicas. Essa distinção delimita o alcance da proposta.
O que a OpenAI afirma ter demonstrado
No manuscrito Finite time blowup for Navier–Stokes, a OpenAI afirma construir, para qualquer viscosidade positiva, um escoamento tridimensional inicialmente em repouso, submetido a uma força suave com suporte compacto no espaço e no tempo.
Segundo o teorema apresentado, a velocidade cresce sem limite em tempo finito, enquanto a energia cinética permanece uniformemente limitada. A concentração do movimento em uma região progressivamente menor ajuda a compreender essa combinação: velocidade local e energia total medem propriedades diferentes do escoamento.
A empresa declara que a construção satisfaz as alternativas C e D do enunciado oficial. O papel da força externa precisa permanecer explícito na divulgação. A construção proposta tem hipóteses determinadas; conclusões sobre outras condições exigem demonstrações próprias.
O anúncio institucional da OpenAI e o repositório com a formalização em Lean permitem consultar os materiais disponibilizados pela empresa.
A crítica divulgada pelo King’s College London
Alexander Bastounis, Fabian Circelli e Anders C. Hansen publicaram, em 6 de outubro de 2026, o preprint Navier–Stokes lost in translation. A comunicação do King’s College London, de 27 de outubro, apresentou suas conclusões ao público. O estudo crítico ainda não havia passado por revisão por pares, conforme a universidade.
Os autores examinam a fidelidade da tradução do texto matemático para Lean. Entre os exemplos, apontam uma discrepância nas estimativas do Lema 8.6: a formalização citada requer uma derivada adicional dos dados de entrada para controlar as derivadas da saída. Isso altera a força da afirmação demonstrada naquele trecho.
Os pesquisadores delimitam expressamente sua conclusão: a análise identifica problemas de correspondência entre as versões. Ela não estabelece que a demonstração escrita inteira esteja errada ou que o resultado anunciado seja falso.
O que significa verificar uma prova matemática
Lean verifica inferências dentro das definições, hipóteses e enunciados formalizados. A avaliação científica também precisa examinar a correspondência desses elementos com o problema original e com o argumento apresentado aos matemáticos.
O caso evidencia uma tarefa essencial para a pesquisa apoiada por inteligência artificial: tornar auditável o caminho entre a descoberta proposta, sua exposição escrita e sua representação formal. A leitura independente desses materiais continua necessária.
Um anúncio que merece acompanhamento
A posição editorial desta matéria é tratar o trabalho como uma solução anunciada, com questões de verificação em discussão. O interesse científico permanece ligado ao exame dos argumentos, à resposta às objeções e ao escrutínio da comunidade matemática.
Nota de revisão: esta matéria reúne a proposta da OpenAI, o enunciado oficial e a análise crítica consultada. Não constitui certificação independente da demonstração.