OpenAI não entende própria prova matemática, dizem especialistas: o caso Navier-Stokes
Matemáticos dizem que a OpenAI não entende sua própria prova do problema de Navier-Stokes. A controvérsia envolve abordagens diferentes e um exército de 10 mil agentes cuja eficácia é incerta.
Em setembro de 2025, a OpenAI apresentou uma solução de 166 páginas para o problema de Navier-Stokes, um dos sete Problemas do Milênio do Clay Mathematics Institute. A empresa afirmou que a prova seguia a abordagem dos matemáticos espanhóis Diego Córdoba e Luis Martínez-Zoroa. Agora, grupos de especialistas contestam essa afirmação.
Resumo
- Especialistas contestam que a prova da OpenAI para Navier-Stokes seja original.
- A OpenAI usou 10 mil agentes, mas ninguém sabe o que eles contribuíram.
- O Clay Institute ainda não validou a prova, que foi escrita em linguagem Lean.
- O caso reforça a necessidade de transparência e reprodutibilidade na ciência.
Segundo a Scientific American, matemáticos apontam que as semelhanças são apenas superficiais. “Quando você vai aos detalhes, é uma abordagem diferente”, disse o matemático Gonzalo Cao-Labora, da EPFL. A prova foi escrita em Lean, uma linguagem de verificação formal que checa cada passo lógico, mas torna o texto quase ileível para humanos. O Clay Mathematics Institute ainda revisa o material.
Antes da publicação, o matemático da NYU Tristan Buckmaster acusou a OpenAI de se basear em trabalho que ele e Levent Alpöge (da Anthropic) haviam feito com modelos públicos. A OpenAI negou, alegando que nunca usou os dados de Buckmaster. Camillo De Lellis, do Institute for Advanced Study, diz que uma resposta definitiva é impossível porque modelos de linguagem são caixas-pretas.
A controvérsia repercutiu entre matemáticos brasileiros, que acompanham o caso com atenção. O debate acendeu alerta em departamentos de matemática do país, especialmente por envolver inteligência artificial na resolução de um dos Problemas do Milênio. Para a comunidade acadêmica brasileira, a transparência e a reprodutibilidade são valores centrais — e o uso de uma linguagem formal como Lean levanta questões sobre o acesso ao conhecimento.
O exército de 10 mil agentes que ninguém entende
A OpenAI usou cerca de 10 mil instâncias de modelo por 88 horas e 130 bilhões de tokens para desenvolver a prova. Mas, de acordo com o pesquisador da OpenAI Noam Brown (em vídeo), ninguém sabe ao certo o que esse enxame massivo de agentes realmente contribuiu. O comportamento nessa escala não foi estudado porque testes comparativos com milhares de agentes custam caro. Brown atribui menos de 10% do sucesso à configuração multiagente; o que importa, diz, é o modelo base, que pode processar tarefas longas em paralelo.
Enquanto a OpenAI jogou um exército de agentes no problema, outras empresas mostram que é possível fazer mais com menos. Por exemplo, a DeepSeek superou o GPT-5.5 Sol em benchmark de codificação com custo bem menor, demonstrando que eficiência pode valer mais que escala bruta.
O que ainda está em aberto
O Clay Mathematics Institute ainda não se pronunciou oficialmente sobre a validade da prova. A comunidade matemática aguarda uma análise independente e questiona se a IA realmente entende a matemática que produziu. Para o Brasil, o caso reforça a importância de investir em pesquisa fundamental e em ferramentas de verificação formal que sejam acessíveis a todos os pesquisadores, não apenas a grandes laboratórios de IA.
O que é Lean? Linguagem de verificação formal que checa cada passo lógico de provas matemáticas.
📲 A história da prova Navier-Stokes ainda pode render reviravoltas. Para saber na hora em que o Clay Institute divulgar o veredito, cola no Canal do TS no WhatsApp.
O debate sobre a prova de Navier-Stokes vai além do resultado em si: ele expõe as dificuldades de confiar em resultados gerados por caixas-pretas e a necessidade de transparência na ciência.
Fonte: The Decoder
Escrito por
