Navier-Stokes é o tipo de problema que separa quem gera texto convincente de quem prova alguma coisa. A OpenAI afirma ter resolvido uma das equações do milênio, com prêmio de 1 milhão de dólares em jogo, em uma prova de 166 páginas escrita em Lean. Só que os matemáticos que ela diz ter seguido afirmam que a empresa não entendeu a própria abordagem que alega ter usado. Para quem opera com IA, o recado é direto: gerar prova formal verificável por máquina é diferente de entender matemática, e essa diferença está explodindo agora em público.

O fato sem enfeite

No início de setembro, a OpenAI publicou uma potencial solução para o problema de existência e suavidade das equações de Navier-Stokes, um dos sete problemas do Clay Mathematics Institute. O documento tem 166 páginas e foi escrito em Lean, uma linguagem de verificação formal que checa cada passo lógico. A empresa disse que seguiu a linha de trabalho dos matemáticos espanhóis Diego Córdoba e Luis Martínez-Zoroa. O instituto está revisando o material desde o lançamento, sem veredito até agora.

PublicidadeAnuncie aqui336x280 / responsivo

O problema veio rápido. Gonzalo Cao-Labora, matemático da EPFL, afirmou que ao entrar nos detalhes a abordagem é outra. As semelhanças seriam apenas superficiais. Antes da publicação, Tristan Buckmaster, da NYU, acusou a OpenAI de ter se apoiado em trabalho que ele desenvolveu com Levent Alpöge, hoje na Anthropic, usando modelos públicos. A OpenAI negou ter usado os dados dele. Camillo De Lellis, do Institute for Advanced Study, resumiu o impasse: como modelos de linguagem são caixas-pretas, uma resposta definitiva sobre contaminação ou inspiração é praticamente impossível.

Em outubro, a situação azedou de vez. A OpenAI despejou cerca de 400 resultados adicionais em uma coleção solta no GitHub. Muita gente boa na matemática viu aquilo como atropelo, uma tentativa de inundar o campo com quantidade em vez de passar pelo ritual lento de revisão, discussão e refino. Não é só vaidade acadêmica. É um choque de cultura entre publicar para validar e publicar para demonstrar escala.

Como funciona na visão de quem opera

Para entender o caso, esqueça por um minuto a equação e olhe para a arquitetura. A prova está em Lean, o que muda tudo. Lean não avalia se a ideia é elegante ou profunda. Ele só deixa compilar se cada inferência for logicamente válida. Isso é ótimo para eliminar erro bobo, mas péssimo para legibilidade humana. Você pode ter 166 páginas que passam no verificador e continuam incompreensíveis para um especialista. É código que compila, mas ninguém consegue fazer code review de verdade.

Do lado da infra, os números são brutais. A OpenAI fala em cerca de 10 mil instâncias de modelo rodando por aproximadamente 88 horas, com consumo na casa de 130 bilhões de tokens para chegar à potencial solução de Navier-Stokes. Em termos de operador, pense em um enxame de agentes tentando lemas paralelos, com um orquestrador selecionando caminhos promissores e descartando becos sem saída. Latência aqui não é tempo de resposta de API, é tempo de busca em árvore de prova. Custo não é centavos por chamada, é um cluster inteiro queimando por dias para explorar um espaço de busca gigantesco.

O ponto mais honesto veio de dentro. O pesquisador Noam Brown admitiu que ninguém sabe de fato o que o enxame de 10 mil agentes contribuiu. Não houve teste controlado comparando um agente contra mil ou dez mil, porque esse teste custaria caro demais para repetir. A estimativa dele é que menos de 10 por cento do sucesso vem do setup multiagente. O que conta mesmo seria o modelo base, capaz de sustentar raciocínio longo e rodar em paralelo. Em outras palavras, a empresa escalou sem instrumento de medição. Funciona, mas ninguém sabe por que funciona nessa escala.

O que isso muda na prática

Quem ganha com isso no curto prazo são os times que já trabalham com verificação formal. Se você atua com software crítico, hardware, criptografia ou assistentes de prova, o recado é claro: modelos capazes de gerar Lean que compila viram ferramenta real de produtividade, mesmo que a criatividade matemática ainda seja questionável. Quem perde são os times que vendiam IA para matemática como se fosse só acertar resposta de olimpíada. Navier-Stokes mostrou que a régua agora é outra. Não basta acertar o final, precisa sustentar a cadeia lógica sem alucinar no meio.

Para laboratórios e empresas, o ajuste é operacional. Não trate prova em Lean como artigo pronto. Trate como pull request gigante sem descrição. Você precisa de pipeline de auditoria humana, com decomposição em lemas menores, testes de robustez e reexecução independente. Se você está construindo produto com agentes para tarefas longas, aprenda com o erro de medição da OpenAI. Antes de sair de mil para dez mil agentes, rode um experimento pequeno e caro uma vez, com grupo controle, para saber seu ganho marginal por agente. Sem isso, você só está queimando token para impressionar em post.

  • Ação prática: se for avaliar prova gerada por IA, exija a árvore de dependências em Lean separada por lemas, rode o verificador em ambiente limpo e peça para dois revisores humanos explicarem a estratégia em linguagem natural sem olhar o código. Se ninguém consegue contar a história da prova em cinco parágrafos, você tem compilação, não compreensão.
  • Regra de custo: modele o custo por lema provado e por lema descartado, não por token total. Em busca massiva, 90 por cento do gasto vai para o lixo. Quem não mede descarte não tem como otimizar orquestração.

A tensão que ninguém quer encarar

Aqui está a dúvida real: isso escala ou só move o gargalo? A promessa era que agentes massivos resolveriam ciência. O que vimos foi um sistema que gera tanto material formal que a comunidade humana não consegue acompanhar. Passamos de escassez de prova para escassez de revisão. Isso resolve o problema da descoberta ou cria um novo problema de validação? Se 400 resultados no GitHub já travam a fila de avaliação, o que acontece quando forem 40 mil?

Tem também a questão do crédito. Se o próprio pesquisador diz que o enxame multiagente responde por menos de 10 por cento, por que a narrativa foi de 10 mil agentes trabalhando juntos? Porque escala vende. É mais fácil anunciar exército de IAs do que explicar melhoria silenciosa em raciocínio longo, memória de prova e busca guiada. Para quem opera, isso é alerta clássico: desconfie quando a arquitetura vira marketing. O ganho real quase sempre está no modelo base e no loop de verificação, não no número bonito de agentes no slide.

E por fim, a contaminação. Se ninguém consegue provar se o modelo viu ou não o trabalho de Buckmaster e Alpöge, como fica a originalidade científica feita por LLM? Na engenharia de software a gente convive com isso com licenças e testes de similaridade. Na matemática do milênio, com 1 milhão de dólares e prestígio eterno em jogo, caixa-preta não é detalhe técnico. É um problema estrutural de atribuição e confiança.

Conclusão

A OpenAI pode ter produzido um artefato impressionante em Lean, mas até agora não convenceu quem entende Navier-Stokes de que entendeu o caminho que diz ter trilhado. Compilar não é compreender, e escalar agentes não é escalar ciência. A pergunta que fica para quem constrói é simples: você prefere um sistema que gera 400 provas que ninguém consegue ler, ou um que gera uma prova que um humano consegue explicar?