A notícia foi apresentada como uma possível solução para um dos Problemas do Milênio. Essa formulação é forte demais para o estado atual da evidência.

A OpenAI anunciou uma prova candidata para uma versão forçada das equações de Navier–Stokes. O trabalho de Tristan Buckmaster, da NYU, e Levent Alpöge, funcionário da Anthropic, avançou em problemas relacionados. As duas histórias se cruzaram depois de uma corrida contra o tempo, com acusações de uso indevido de informações e uma disputa ainda aberta sobre autoria e prioridade.

O resultado matemático pode ser importante. O processo que levou até ele é o que merece mais atenção.

O problema

As equações de Navier–Stokes descrevem o movimento de fluidos como água e ar. Elas combinam pressão, viscosidade, transporte de quantidade de movimento e forças externas.

O problema do Milênio pergunta se um fluido tridimensional, incompressível e inicialmente suave permanece suave para sempre. A alternativa é que uma singularidade apareça em tempo finito: uma grandeza como a velocidade cresce sem limite em uma região cada vez menor.

A viscosidade tende a suavizar o fluido. Os termos não lineares podem concentrar o movimento. A dificuldade está em saber qual efeito vence em três dimensões.

O Clay Mathematics Institute ainda classifica o problema como não resolvido. A formulação oficial divide a questão em alternativas sobre existência global, regularidade e formação de singularidades.

O avanço matemático

A linha de ataque veio de um programa desenvolvido por Diego Córdoba e Luis Martínez-Zoroa. A ideia usa uma sequência de camadas regulares que, combinadas, concentram o movimento e produzem uma singularidade.

Os resultados anteriores tinham um obstáculo: a força externa necessária para produzir o blow-up podia deixar de ser suave. A formulação do Clay exige uma construção mais controlada.

Buckmaster e Alpöge publicaram resultados para três equações relacionadas:

  • Euler tridimensional incompressível;
  • Boussinesq;
  • meios porosos incompressíveis, ou IPM.

Eles afirmam também ter uma prova para uma versão dissipativa de Navier–Stokes, mas disseram que a formalização em Lean ainda não estava concluída. O trabalho usou Claude, Codex e Astra. Na declaração de Buckmaster, o resultado de Euler já havia sido verificado em Lean, embora os textos publicados ainda estivessem pouco trabalhados.

A equipe também reconhece que a ideia fundamental veio de Córdoba e Martínez-Zoroa. A contribuição de Buckmaster e Alpöge foi levar o programa até forças suaves e novas equações.

O anúncio da OpenAI

A OpenAI diz que ouviu rumores sobre avanços em problemas do Milênio em 1º de setembro. Depois disso, colocou um modelo interno para testar vários desses problemas.

O sistema usou grupos de agentes com acesso a código, uma cópia em cache da internet e comunicação entre si. Para Navier–Stokes, a OpenAI relata:

  • cerca de 10 mil agentes concorrentes;
  • 88 horas até a prova candidata;
  • 17 horas adicionais para a formalização em Lean;
  • 2,7 milhões de mensagens entre agentes;
  • aproximadamente 130 bilhões de tokens de saída.

A construção anunciada usa um vórtice que espirala para dentro e se alonga. A região central encolhe enquanto a velocidade cresce. A força externa permanece suave e a energia continua finita, segundo a descrição da empresa.

A OpenAI diz que a prova corresponde às alternativas C e D da formulação de Fefferman e que não pretende reivindicar o prêmio de US$ 1 milhão.

O que Lean verifica

A formalização em Lean é uma evidência forte. Ela verifica que, dentro das definições, hipóteses e lemas codificados, a conclusão decorre logicamente.

Isso ainda não encerra a revisão. Matemáticos precisam confirmar que:

  • o enunciado formal corresponde ao problema do Clay;
  • as condições iniciais e o domínio são os exigidos pela formulação oficial;
  • a força externa é realmente suave no sentido correto;
  • não houve uma hipótese mais forte que tenha tornado o problema mais fácil;
  • a prova produz o fenômeno reivindicado, e não uma variante próxima.

Lean reduz o risco de erro formal. Não substitui a leitura matemática nem garante que o código formalizou exatamente a pergunta que a comunidade queria responder.

A disputa sobre proveniência

Buckmaster afirma que ele e Alpöge trabalhavam havia quase um ano e obtiveram um avanço importante em agosto. Segundo seu relato, informações sobre esse trabalho chegaram à OpenAI antes de a empresa iniciar a busca específica.

Ele perguntou se os modelos haviam sido treinados com as sessões do Codex nas quais a dupla guardava rascunhos e provas. Diz que recebeu a resposta de que o modelo não consultava dados de usuário, mas não obteve uma resposta clara sobre o possível uso desses dados em treinamento.

A posição publicada pela OpenAI é mais limitada: a empresa diz que não acessou dados específicos de usuários para resolver o problema, mas admite que não pode descartar completamente que dados desidentificados derivados do uso de seus produtos tenham contribuído para melhorar os modelos.

As duas afirmações não são equivalentes. “O agente não consultou diretamente o seu rascunho” não responde completamente à pergunta “o rascunho ou seus derivados puderam influenciar o treinamento?”.

A OpenAI também afirma que não viu o trabalho da dupla antes de ele se tornar público e que sua prova difere matematicamente dos resultados de Euler publicados por eles. A cronologia e a extensão dessa separação ainda precisam ser esclarecidas.

Autoria e conduta

Buckmaster relata que a OpenAI ofereceu esperar a publicação deles ou permitir que ele escrevesse um artigo sobre o resultado da empresa. Segundo ele, Alpöge seria excluído da autoria por trabalhar na Anthropic.

Buckmaster também relata frases ameaçadoras durante as conversas. Sébastien Bubeck, da OpenAI, negou as acusações e as classificou como falsas e inflamatórias. Depois, disse que se desculpava pela escolha das palavras, embora mantivesse uma versão diferente sobre o conteúdo da conversa.

Essa parte não pode ser tratada como fato estabelecido. Existem relatos incompatíveis, e o público não viu a prova da OpenAI nem os registros completos das conversas. A alegação, contudo, é grave o suficiente para exigir investigação independente, não apenas uma disputa em redes sociais.

A versão forçada resolve o Problema do Milênio?

Ainda não se pode afirmar isso. Mas a razão é mais interessante do que “tem força externa, então não vale”.

A formulação oficial de Fefferman divide o problema em quatro alternativas. As duas positivas, existência e suavidade globais em R³ e no toro, exigem que a força externa seja identicamente nula. As duas negativas, (C) e (D), que pedem a construção de uma singularidade, admitem uma força externa, desde que ela seja suave e satisfaça limites estritos de decaimento em todas as derivadas.

Ou seja: a rota que a OpenAI diz ter percorrido está dentro do enunciado. A pergunta correta não é “com ou sem força”, mas se aquela força específica cabe nos limites que Fefferman impôs. É uma verificação técnica concreta, e é exatamente por isso que a ausência do manuscrito completo importa tanto.

Dito isso, a distância entre o caso forçado e o não forçado não é burocrática.

Stan Palasek, de Princeton, apontou um obstáculo em uma das rotas propostas para eliminar o forçamento: em uma construção baseada em instabilidades acopladas em frequências muito separadas, a perda viscosa de energia superaria o mecanismo de crescimento. Terence Tao acolheu a observação e sugeriu estudar um modelo mais simples para tornar as interações explícitas.

A objeção de Palasek não refuta um resultado forçado que satisfaça as condições do Clay, nem encerra todas as rotas possíveis para o caso não forçado. Ela mostra outra coisa: remover a força não é um passo de arredondamento. É um problema aberto com resistência própria.

Vale registrar também o que Tao disse antes do anúncio da OpenAI. Ele descreveu o programa de Alpöge e Buckmaster como uma conquista notável e afirmou não ver obstáculo óbvio à extensão dos métodos até Navier–Stokes completo, ressalvando a enorme dificuldade técnica envolvida. Uma via promissora não elimina o trabalho de fazer todas as estimativas fecharem.

O Clay continua listando o problema como não resolvido. Pelas regras do instituto, uma solução precisa ser publicada, passar por revisão da comunidade e sobreviver ao período de avaliação previsto antes de qualquer premiação.

O que esse caso muda

A conquista, se confirmada, mostra que agentes podem trabalhar em uma cadeia de pesquisa matemática: testar variações, encontrar lemas, compartilhar resultados, descartar caminhos e consolidar uma prova formal.

Mas o caso também expõe uma falha de governança. A prova pode ser auditável em Lean e a trajetória de descoberta continuar opaca.

Um sistema científico baseado em agentes precisa registrar, de forma verificável:

  • quais dados cada agente acessou;
  • quando cada linha de investigação começou;
  • quais modelos e versões foram usados;
  • quais humanos forneceram ideias ou direcionamento;
  • como foram tratados dados de usuários;
  • como a autoria e a prioridade foram atribuídas.

Sem essa trilha, a comunidade pode até validar o teorema, mas não consegue reconstruir de maneira confiável como ele foi obtido.

Esse é o precedente mais importante do episódio. A OpenAI estimou o custo computacional do esforço em alguns milhões de dólares. Agentes reduzem o custo de transformar um rumor em uma corrida de computação. A partir de agora, uma equipe pode perder prioridade não porque outra equipe teve uma ideia melhor, mas porque ouviu que a primeira estava perto e conseguiu mobilizar mais máquinas.

Simon Willison fez uma analogia útil com segurança ofensiva: quando um pesquisador descobre que existe uma vulnerabilidade, o rumor de um erro não corrigido já pode levar agentes a procurar uma exploração. Em pesquisa, saber que existe uma solução não publicada pode produzir o mesmo efeito. O incentivo deixa de ser apenas descobrir e passa a ser chegar primeiro, antes que outra equipe consiga mobilizar mais agentes e mais recursos.

O que mudaria minha avaliação

Três fatos mudariam a avaliação cautelosa deste texto: a publicação do manuscrito completo da OpenAI; a leitura independente do enunciado formal em Lean por especialistas em equações de fluidos; e uma resposta objetiva, verificável e auditável sobre se dados das sessões de Buckmaster e Alpöge participaram do treinamento ou da seleção da estratégia.

Até lá, há uma diferença entre validar a lógica de uma prova formalizada e validar a reivindicação científica, a cronologia da descoberta e a legitimidade do processo que a produziu.

A matemática ainda precisa decidir se a prova está correta. A comunidade científica também precisa decidir quais regras tornam legítima uma descoberta produzida dessa maneira.

Fontes