OpenAI diz ter resolvido Navier–Stokes: o que foi provado de fato

A OpenAI anunciou em 8 de setembro de 2026 que um sistema de agentes rodando um modelo interno produziu uma prova de que as equações de Navier–Stokes, que descrevem o movimento de fluidos, podem desenvolver uma singularidade: um fluido que parte do repouso e, empurrado por uma força externa suave, atinge velocidade infinita em tempo finito. Se a prova se confirmar, é a primeira vez que uma IA resolve um dos Problemas do Milênio do Clay Mathematics Institute, cada um com prêmio de US$ 1 milhão. Mas a história tem três ressalvas. O resultado vale para a versão do problema com força externa, não para a pergunta sem força. Dois matemáticos dizem que a OpenAI correu atrás do problema depois de saber do trabalho deles. E a checagem independente ainda não terminou.

O que a OpenAI anunciou?

O comunicado da empresa diz que a prova foi produzida por um modelo interno "significativamente mais capaz" que o GPT-6 Astra, lançado cinco dias antes, e veio acompanhada de um texto matemático de 166 páginas e de uma formalização em Lean, linguagem em que o computador confere cada passo de uma demonstração. O código está num repositório público no GitHub, com instruções para checagem independente.

Segundo a OpenAI, o trabalho começou em 1º de setembro, depois de a empresa ouvir rumores de que dois Problemas do Milênio teriam sido resolvidos. A equipe pôs grupos de agentes para atacar todos os problemas em aberto e algumas questões mais fáceis. Uma delas, a explosão das equações de Euler (Navier–Stokes sem viscosidade) sem força externa, caiu primeiro: perto de 100 agentes levaram cerca de 50 horas. A empresa então concentrou os recursos em Navier–Stokes.

O grupo que chegou à prova tinha da ordem de 10 mil agentes trabalhando ao mesmo tempo. A resolução saiu no sábado, 5 de setembro, cerca de 88 horas depois do lançamento dos primeiros agentes, e a formalização em Lean levou mais 17 horas, feita com o GPT-6 Astra. Só nesse problema, os agentes trocaram 2,7 milhões de mensagens e geraram aproximadamente 130 bilhões de tokens de saída. Sébastien Bubeck, da OpenAI, estimou à Quanta Magazine o custo computacional em vários milhões de dólares. A empresa afirma que não vai reivindicar o prêmio.

O que exatamente foi provado?

O enunciado oficial do problema, escrito por Charles Fefferman, de Princeton, em 2000, aceita quatro respostas. As alternativas A e B pedem provar que, sem nenhuma força externa, qualquer fluido que começa suave continua suave para sempre, no espaço inteiro (A) ou numa caixa periódica (B). As alternativas C e D pedem o contrário: mostrar que existe algum estado inicial suave e alguma força externa suave para os quais a solução quebra. Provar qualquer uma das quatro resolve o problema.

O teorema principal do paper da OpenAI constrói, para qualquer viscosidade positiva, um fluido que parte do repouso, recebe uma força suave e concentrada numa região limitada do espaço e do tempo, mantém a energia cinética finita e, mesmo assim, tem velocidade ilimitada num instante finito. Isso estabelece a alternativa C; por ser tudo concentrado numa região limitada, a construção também vale para a caixa periódica, a alternativa D. A solução é um vórtice que gira para dentro e se alonga, "como espaguete", nas palavras do comunicado, enquanto termos enormes das equações se cancelam com precisão para que a força aplicada continue suave.

A pergunta sem força externa, a de A e B, continua em aberto. Isso não diminui o resultado do ponto de vista do prêmio, já que o enunciado aceita C e D, mas explica por que vários matemáticos tratam a conquista com cautela. A ideia de construir explosões controlando a força externa vem de Diego Córdoba e Luis Martínez-Zoroa, que a desenvolvem há anos. Fefferman disse à Quanta que ficou "empolgado" com a solução e chamou os dois de "heróis da história".

Por que há uma disputa de crédito?

Na noite de 7 de setembro, cerca de 12 horas antes da OpenAI, Tristan Buckmaster, professor da NYU, e Levent Alpöge, funcionário da Anthropic, publicaram três resultados: explosão com força suave para as equações de meios porosos incompressíveis, de Boussinesq e de Euler em três dimensões. Os dois trabalhavam havia cerca de um ano no programa de Córdoba e Martínez-Zoroa, com ajuda de modelos da Anthropic e da OpenAI, pagos com verbas de pesquisa do próprio Buckmaster. Segundo a declaração dele, os resultados de Euler e Boussinesq saíram em 15 de agosto e foram verificados em Lean em 22 de agosto.

Na mesma declaração, Buckmaster conta que, em 3 de setembro, com rumores circulando, escreveu a um matemático da OpenAI. Em 6 de setembro, em duas ligações com a participação de Bubeck, soube que um modelo interno tinha provado a versão com força de Navier–Stokes. Ele diz que lhe mostraram um prompt e afirmaram que o modelo recebera só o enunciado, e que Alpöge ouviu de Bubeck que houve "muito pouca intervenção humana". Ao longo da conversa, segundo Buckmaster, ficou claro que havia uma equipe inteira trabalhando e "uma quantidade insana de computação". Perguntou se o modelo tinha sido treinado com as sessões do Codex em que ele e Alpöge guardavam os rascunhos, e diz que não teve resposta sobre treino.

A OpenAI nega ter visto o trabalho dos dois. O comunicado afirma que nem os pesquisadores nem os agentes tiveram acesso a ele antes da publicação e que nenhum dado específico de usuário foi acessado, mas admite que não pode "descartar" que dados desidentificados do uso dos seus produtos tenham ajudado a melhorar os modelos. A empresa reconhece a prioridade de Buckmaster e Alpöge no caso de Euler com força e diz que as provas são bem diferentes. Na entrevista coletiva, Bubeck declarou: "Não usamos o prompt nem as provas deles para instruir nossos modelos".

Dias antes, em 3 de setembro, Terence Tao tinha publicado um alerta que soou premonitório. Para ele, uma solução produzida por IA sem transparência sobre o processo pode "contaminar" o trabalho que costuma nascer da tentativa de resolver esses problemas, a ponto de virar "um saldo negativo" para a matemática.

A prova já foi verificada?

Não de forma independente e definitiva. Lean garante que a prova formal está correta, mas alguém precisa confirmar que o enunciado formal diz o mesmo que o problema original e que o texto em linguagem natural. Em 6 de outubro, Alexander Bastounis, Fabian Circelli e Anders C. Hansen publicaram no arXiv um artigo argumentando que traduzir automaticamente matemática para Lean pode não dar confiança nenhuma no argumento original e afirmando que, no caso da OpenAI, a prova formalizada "não corresponde" à prova em linguagem natural. É uma crítica ainda sem resposta pública detalhada da empresa, e não um consenso.

O Clay, por sua vez, não tem pressa. O regulamento do prêmio exige que a solução seja publicada num veículo qualificado, que passem pelo menos dois anos da publicação e que haja aceitação geral da comunidade matemática. Na página do instituto, Navier–Stokes continua listado como problema ativo.

A própria OpenAI ajustou o tom. Em 6 de outubro, ao divulgar um pacote de outros resultados matemáticos, a empresa disse estar seguindo recomendações de um grupo consultivo independente sobre matemática e IA do Institute for Advanced Study, publicando as provas num repositório com regras de revisão e citação. No mesmo texto, o caso de Navier–Stokes aparece descrito como um modelo que "propõe uma solução".

O que isso muda?

Mesmo com as ressalvas, o episódio marca uma mudança de escala. Buckmaster, que perdeu a corrida, escreveu que o mais importante não é o resultado, e sim o fato de que um matemático e um modelo agora fazem esse trabalho em um mês, e chamou a situação de "um momento Deep Blue-Kasparov". Do lado da OpenAI, foram 88 horas com milhares de agentes.

Há duas consequências práticas. A primeira é sobre quem pode atacar problemas desse porte: com custos de vários milhões de dólares em computação, poucas instituições fora das grandes empresas de IA conseguem competir. A segunda é sobre crédito e confiança: modelos usados por pesquisadores acadêmicos são operados pelas mesmas empresas que agora disputam os mesmos problemas, e as regras de uso de dados viraram parte da discussão científica.

Para quem acompanha IA, o recado é que matemática de fronteira deixou de ser um teste distante. Antes deste anúncio, o comunicado do GPT-6 Astra já dizia que o modelo tinha ajudado a resolver problemas antigos em aberto. Agora a pergunta é menos se a IA consegue e mais como a comunidade vai verificar, creditar e aprender com provas que nenhum humano escreveu.