Navier-Stokes sempre foi aquele tipo de desafio que separa matemática de verdade de exercício de benchmark. A pergunta é simples de enunciar e brutal de responder: uma solução suave das equações incompressíveis em três dimensões pode desenvolver velocidade infinita em tempo finito, ou ela permanece suave para sempre? Por décadas, isso travou gente muito boa. Não por falta de computação, mas porque exige construir um exemplo explícito de blowup, com controle rigoroso de energia, vorticidade e condição de contorno. É exatamente aí que a OpenAI decidiu entrar, dizendo que resolveu o caso forçado com um modelo interno ainda não lançado.

Para quem opera com IA, o incômodo começa antes da matemática. A empresa afirma que partiu de quase zero em dinâmica de fluidos, escalou para cerca de 10 mil agentes concorrentes e fechou uma prova formalizada em Lean em poucos dias. Se isso for sólido, muda a conversa sobre o que agente autônomo faz em pesquisa profunda. Se for apressado, vira só mais um episódio de laboratório usando problema famoso como outdoor. E tem a briga por crédito, que já contaminou tudo.

PublicidadeAnuncie aqui336x280 / responsivo

O fato: o que a OpenAI diz que fez

A sequência divulgada pela empresa é agressiva. Em 1 de setembro, depois de rumores de que dois problemas do Millennium teriam sido resolvidos, a OpenAI teria lançado um esforço com agentes sobre os problemas em aberto. Quase 100 agentes teriam resolvido primeiro a questão do blowup de Euler sem forçamento em cerca de 50 horas. Depois disso, o foco migrou para Navier-Stokes, com escala massiva de paralelismo.

Em 5 de setembro, segundo a OpenAI, os agentes chegaram a uma resolução cerca de 88 horas após o início. A formalização e verificação em Lean teriam levado mais 17 horas usando o GPT-6 Astra. No total da semana, contando todos os problemas atacados, o consumo teria sido de 300 bilhões de tokens de saída, avaliados em cerca de 22,5 milhões de dólares nas tarifas atuais do Astra. Em 8 de setembro, a empresa publicou prova, preprint e arquivos Lean. O mecanismo descrito é visual: um vórtice que espirala para dentro e estica como espaguete, com o núcleo encolhendo e acelerando até o blowup em um fluido inicialmente em repouso, com força externa suave e energia finita.

O Clay Mathematics Institute, que colocou o prêmio de 1 milhão de dólares em 2000, mantém o problema como não resolvido até escrutínio prolongado e aceitação ampla. A OpenAI disse que não vai reivindicar o prêmio. Só que dois dias antes, em 7 de setembro, Tristan Buckmaster, da NYU, e Levent Alpöge, matemático ligado à Anthropic, publicaram um resultado de blowup para Euler forçado obtido principalmente com Codex da OpenAI e Claude. A sobreposição de datas acendeu a disputa.

Como funciona: 10 mil agentes e 300 bilhões de tokens

Olhando como operador, o número que importa não é o prêmio, é a arquitetura implícita. Dez mil agentes concorrentes não significa dez mil pesquisadores pensando. Significa um orquestrador gerando hipóteses de construção, tentando estimativas de energia, descartando becos sem saída e refinando lemas em paralelo. O mais plausível é um pipeline com planejador central, workers especializados em análise PDE, busca de contraexemplos numéricos e tradução para Lean, além de um verificador que rejeita passos inválidos. Latência aqui não é de resposta de chatbot, é de iteração de prova: propor, testar numericamente, tentar formalizar, falhar rápido.

O custo conta a mesma história. Trezentos bilhões de tokens de saída em uma semana é ordem de grandeza de pré-treinamento curto, queimado em inferência. Mesmo com batching agressivo e cache, isso sugere dezenas de milhões em computação se cobrado a preço cheio. Faz sentido para um golpe de marketing científico, não faz sentido como rotina de laboratório universitário. Nenhum grupo acadêmico vai rodar esse volume para cada conjectura. A inferência técnica é que a OpenAI usou um modelo interno descrito como significativamente mais capaz que o GPT-6 Astra como gerador, e o Astra como verificador e formalizador. Isso explicaria a divisão: criatividade pesada na frente, checagem rigorosa atrás.

Onde entra o Lean nisso

O Lean muda o jogo porque tira parte da discussão do campo do 'acredite em mim'. A formalização obriga cada passo a passar no checador de tipos, o que reduz erro humano em desigualdades longas e argumentos de escala. Foram 17 horas de verificação com o Astra, o que indica automação forte de táticas e preenchimento de lacunas, não digitação manual. Ainda assim, Lean prova que a lógica interna fecha, não que a modelagem do problema está certa ou que a interpretação física é nova. É um selo de consistência poderoso, mas não substitui revisão por especialistas em blowup, que vão caçar hipótese escondida, regularidade na fronteira e controle de força externa.

O que isso muda na prática

Quem ganha de imediato é quem trabalha com prova assistida e descoberta científica. Se o pipeline for reprodutível, mesmo em escala menor, laboratórios de matemática aplicada, CFD e controle podem adaptar a ideia: usar LLM para propor construções, solver numérico para filtrar intuição e Lean ou Isabelle para travar o resultado. Quem perde, no curto prazo, é quem vende automação de pesquisa como se fosse só plugar API. O recado é que precisa de orquestração pesada, avaliação numérica séria e orçamento de inferência alto. Não é um prompt esperto, é infraestrutura.

  • Pesquisadores: comecem a versionar prompts, seeds e trajetórias de agente como se fossem código experimental, porque disputa de prioridade vai virar rotina.
  • Times de engenharia: testem formalização em Lean em um lema pequeno do seu domínio antes de sonhar com prova completa, para medir custo real por lema verificado.
  • Gestores: tratem resultado de agente em matemática como pré-print interno até revisão externa, nunca como entrega final.

A ação prática mais direta é simples: se você opera com agentes de pesquisa, crie agora um protocolo de proveniência. Registre quando o esforço começou, quais dados externos foram acessados, quais ferramentas foram usadas e o que é contaminação potencial. A OpenAI disse que nem pesquisadores nem agentes viram o trabalho da dupla antes da publicação e que nenhum dado específico de usuário foi acessado, embora não descarte que dados anonimizados de uso tenham ajudado a melhorar modelos. Uma atualização de 10 de setembro afirmou que prompts do Codex de Buckmaster nos dois meses anteriores não poderiam ter influenciado o resultado. Mesmo assim, sem log público, fica palavra contra palavra. Proveniência vai virar compliance de pesquisa.

A briga que mancha o resultado

Buckmaster afirma que ele e Alpöge passaram meses na rota forçada e que quase ninguém mais trabalhava nisso. Ele diz que, ao pressionar a OpenAI sobre quando o esforço começou, as respostas foram evasivas até se concordar que o primeiro prompt foi enviado depois que informações sobre o trabalho deles chegaram à empresa. Ele também alegou que Sébastien Bubeck pediu para remover o crédito de Alpöge e, ao ser confrontado sobre ir a público, teria dito 'Why would you ruin your career?'. Bubeck chamou as alegações de falsas e inflamatórias e disse que o time da OpenAI não tinha expertise em dinâmica de fluidos em nível de pesquisa. Luis Martínez Zoroa, da CUNEF, chamou o resultado de verdadeiramente notável, mas o mérito técnico ficou em segundo plano.

A reação da comunidade foi dura. Terence Tao criticou laboratórios por tratar problemas famosos como peça de marketing. Vinte e cinco medalhistas Fields assinaram carta aberta alertando que anúncios apressados levantam questões graves de atribuição e plágio. Na quinta-feira seguinte, a OpenAI retirou patrocínio de um evento de matemática no Caltech após críticas de pesquisadores. Isso revela a tensão real: dá para escalar descoberta com 10 mil agentes, mas dá para escalar confiança no mesmo ritmo? Custo de 22,5 milhões por semana resolve um gargalo e cria outro, o gargalo da verificação humana, da reputação e da governança de dados de uso. A matemática não aceita 'move fast' sem pagar juros.

Conclusão

No fim, temos uma prova que parece formalmente forte, um custo operacional absurdo e uma disputa ética que ninguém conseguiu encerrar. O avanço técnico pode ser real e o processo pode continuar problemático. A pergunta que fica para quem constrói é direta: você conseguiria reproduzir 1 por cento desse pipeline com orçamento normal, ou isso só funciona como demonstração de força de quem tem cluster sobrando?