Uma carta pública assinada por 25 medalhistas Fields criticou anúncios apressados de matemática gerada por inteligência artificial em 12 de setembro de 2026, quatro dias depois de a OpenAI publicar uma alegação ambiciosa sobre o problema de Navier–Stokes. A empresa afirma ter produzido uma prova analítica e uma formalização em Lean, mas o resultado ainda não é uma solução matematicamente aceita de forma independente.
O episódio não é apenas uma disputa sobre capacidade de IA. Ele coloca na mesma mesa três perguntas diferentes: o que a OpenAI afirma ter demonstrado, o que o Lean realmente consegue verificar e como prioridade, autoria e uso de dados devem ser tratados quando máquinas participam da pesquisa.
O que a OpenAI afirma exatamente
A OpenAI afirma ter construído um exemplo em que um fluxo tridimensional, incompressível e de densidade constante, com forçamento externo suave, desenvolve uma singularidade em tempo finito enquanto sua energia permanece finita. Em linguagem menos intimidadora: partindo de um estado suave, a velocidade do modelo se torna ilimitada em um intervalo finito, segundo a descrição da empresa.
O objeto central seria um vórtice que espirala para dentro e se alonga pelo eixo. Isso pertence ao modelo matemático — não significa que água real ou suas moléculas possam atingir velocidade infinita.
A empresa publicou uma prova analítica e uma formalização em Lean em 8 de setembro de 2026. Essa publicação é um fato; a aceitação do resultado pela comunidade matemática é outra questão, que continua pendente.
Por que Navier–Stokes é um problema do Milênio
As equações de Navier–Stokes descrevem matematicamente o movimento de fluidos. O problema de existência e regularidade em três dimensões pergunta, em termos gerais, se uma evolução inicialmente suave pode permanecer regular ou desenvolver uma singularidade em tempo finito.
O Clay Mathematics Institute inclui essa questão entre os sete Problemas do Prêmio do Milênio, cada um associado a um prêmio de US$ 1 milhão. A OpenAI afirma que não reivindicará o prêmio por esse resultado.
A distinção é importante: publicar uma construção que a própria empresa considera uma resolução não equivale a cumprir, aos olhos da comunidade, todos os critérios matemáticos do problema. A questão também não se transforma automaticamente em uma nova técnica para previsão do tempo, aerodinâmica ou engenharia. O significado imediato é matemático e metodológico.
10 mil agentes e 88 horas
Segundo a OpenAI, o grupo que produziu o resultado reuniu aproximadamente 10 mil agentes simultâneos e chegou à resolução relatada cerca de 88 horas depois do início da avaliação. A formalização e a checagem em Lean teriam exigido mais 17 horas, com participação do GPT-6 Astra.
No esforço dedicado a Navier–Stokes, a empresa contabiliza cerca de 2,7 milhões de mensagens e aproximadamente 130 bilhões de tokens de saída. Em todas as questões tentadas no projeto, os números informados chegam a 4,9 milhões de mensagens e 300 bilhões de tokens.
Essas cifras mostram a escala do experimento, não sua correção nem sua eficiência em comparação com matemáticos humanos. Também ajudam a entender por que a carta dos medalhistas Fields trata o episódio como uma mudança no modo de produzir e divulgar conhecimento: a velocidade da máquina pode ser muito maior que a velocidade necessária para a comunidade compreender, testar e contextualizar uma ideia.
Duas linhas de pesquisa, não uma única prova
A controvérsia também envolve o trabalho de Tristan Buckmaster e Levent Alpöge, que estudavam resultados relacionados sobre as equações de Euler com forçamento e as equações de Boussinesq, com auxílio de IA. Esses objetos matemáticos não devem ser confundidos com a alegação da OpenAI sobre Navier–Stokes.
| Dimensão | Resultado relatado pela OpenAI | Trabalho relacionado de Buckmaster e Alpöge |
| Alvo matemático | Singularidade em tempo finito para Navier–Stokes tridimensional com forçamento suave | Resultados de blow-up relacionados para Euler com forçamento e Boussinesq |
| Ferramentas de IA | Sistema interno com agentes coordenados e formalização posterior em Lean pelo GPT-6 Astra | Claude e Codex como assistentes de pesquisa, documentação e etapas lógicas |
| Relação entre os resultados | A OpenAI afirma que seu resultado tem escopo substancialmente diferente | Buckmaster relaciona a escolha da direção de pesquisa à prioridade de seu trabalho |
Buckmaster alega que a OpenAI tomou conhecimento da direção de seu trabalho, tratou mal as discussões sobre prioridade e não esclareceu inicialmente se dados derivados de sessões do Codex poderiam ter contribuído para o treinamento ou a melhoria dos modelos. A OpenAI nega que seus pesquisadores ou agentes tenham visto o trabalho privado específico antes de sua divulgação pública.
Essas duas afirmações tratam de caminhos diferentes. A OpenAI diz que nenhum dado específico de usuário foi acessado para resolver o problema e, separadamente, afirma não poder descartar que dados desidentificados derivados do uso de seus produtos tenham ajudado a melhorar seus modelos. Essa possibilidade não equivale a uma admissão de acesso direto ao trabalho nem resolve a disputa sobre crédito.
O que o Lean realmente verifica
O Lean é um assistente de provas: ele pode verificar se uma prova formalizada segue das definições, axiomas e hipóteses que foram codificados. É uma barreira importante contra erros dentro daquele sistema formal.
Mas há uma diferença crucial entre verificar uma implementação e decidir se ela representa exatamente a pergunta relevante. A checagem não substitui, por si só, a análise de escopo, a leitura matemática por especialistas nem a compreensão independente do argumento. É por isso que “formalizado em Lean” não significa automaticamente “aceito como solução do problema do Milênio”.
A objeção técnica apresentada por Stan Palasek concentra-se justamente na passagem de uma construção com força externa para a formulação exigida no problema de Navier–Stokes. A questão permanece técnica e disputada; não é uma conclusão de que a prova esteja errada.
A animação selecionada ajuda a visualizar o comportamento de espiral e alongamento descrito na alegação, mas uma visualização não valida a prova. O trabalho decisivo continua sendo a leitura matemática do argumento e de sua formalização.
A advertência dos 25 medalhistas Fields
A carta publicada em 12 de setembro por 25 medalhistas Fields amplia o foco para além de OpenAI e Buckmaster. Os signatários criticam a divulgação acelerada de resultados produzidos com IA, a atribuição insuficiente, a citação fraca de trabalhos anteriores e o pouco tempo destinado à compreensão conceitual.
O ponto não é que a participação de uma máquina torne uma descoberta inválida. O problema é o descompasso entre produzir uma saída e transformá-la em conhecimento compartilhado. Uma prova precisa ser legível, examinável, corretamente situada na história da área e atribuída às pessoas e ideias que contribuíram para ela.
Essa preocupação também explica por que a disputa de crédito não é um detalhe de bastidor. Se sistemas capazes de explorar milhares de caminhos publicam resultados em ritmo acelerado, regras claras sobre prioridade, dados de treinamento e autoria deixam de ser conveniência editorial. Tornam-se parte da infraestrutura da ciência.
O que muda para o leitor
Por enquanto, a conclusão responsável é direta: a OpenAI publicou uma alegação tecnicamente ambiciosa sobre Navier–Stokes, acompanhada de uma prova analítica e de uma formalização em Lean; a aceitação matemática independente ainda não está definida.
O caso também não demonstra que a OpenAI tenha usado indevidamente o trabalho privado de Buckmaster e Alpöge. A empresa nega acesso direto, admite apenas a possibilidade de contribuição indireta de dados desidentificados para a melhoria de modelos, e a disputa de prioridade continua sem resolução pública.
O próximo teste não é contar mais agentes nem produzir mais tokens. É permitir que matemáticos examinem o argumento, confirmem seu escopo e estabeleçam como o resultado se relaciona com as contribuições anteriores. Só então será possível separar uma demonstração aceita de uma demonstração apenas anunciada — e decidir que lugar essa nova forma de pesquisa merece na matemática.
