A OpenAI afirma que seu sistema encontrou uma singularidade em tempo finito nas equações de Navier–Stokes, sob condições específicas: o fluido começa suave e em repouso, há uma força externa suave e a energia permanece finita. Um preprint publicado em 6 de outubro de 2026 contesta a correspondência entre a formalização em Lean e a prova escrita pela empresa.
O que a OpenAI afirma ter provado
Navier–Stokes é um conjunto de equações que descreve o movimento de fluidos. Em 8 de setembro de 2026, a OpenAI publicou sua alegação de que um sistema interno produziu uma prova analítica de uma singularidade em tempo finito nas equações incompressíveis tridimensionais. Uma singularidade desse tipo ocorre quando a solução deixa de ser suave durante a evolução do fluido.
A empresa especificou que o fluido parte de um estado suave e em repouso, sob uma força externa suave, e que sua energia permanece finita. A OpenAI identifica o resultado com as afirmações C e D da formulação do problema do Clay Mathematics Institute. No mesmo anúncio, disse que não pretende reivindicar o prêmio Millennium de US$ 1 milhão.
A OpenAI relatou que cerca de 10 mil agentes chegaram ao resultado após aproximadamente 88 horas de trabalho. A formalização e a verificação em Lean, feitas com o GPT-6 Astra, levaram mais 17 horas, segundo a empresa. Lean é uma linguagem formal usada para escrever provas que um assistente de provas pode verificar.
Euler e Navier–Stokes têm condições diferentes
Os resultados discutidos envolvem equações e condições de força distintas. O trabalho de Tristan Buckmaster e Levent Alpöge sobre Euler foi descrito como forçado; o resultado de Euler da OpenAI, como não forçado. Já a construção de Navier–Stokes apresentada pela OpenAI usa uma força externa suave.
| Resultado | Equação | Condição da força externa |
| Trabalho de Buckmaster e Alpöge | Euler | Forçada |
| Resultado da OpenAI | Euler | Não forçada |
| Resultado da OpenAI | Navier–Stokes | Força suave |
Essa diferença importa porque um resultado para uma equação ou condição de força não descreve automaticamente os demais. A alegação sobre Navier–Stokes é a que a OpenAI relaciona às afirmações C e D do problema do Clay.
Uma reportagem da Scientific American publicada em 22 de outubro de 2026 descreveu avaliações divergentes sobre a relação entre os trabalhos. Buckmaster considerou que a pesquisa da OpenAI continuava uma linha aberta por seu trabalho com Alpöge; outros especialistas apontaram que a construção de Navier–Stokes com força da OpenAI seguia uma rota distinta do programa espanhol.
O que a crítica sobre Lean questiona
Os autores Alexander Bastounis, Fabian Circelli e Anders C. Hansen argumentam, no preprint publicado em 6 de outubro, que a formalização em Lean da OpenAI não corresponde à prova em linguagem natural. A crítica trata da correspondência entre o texto matemático e o enunciado codificado para verificação.
Essa correspondência é importante porque o assistente de provas verifica a proposição formalizada. Para que essa checagem sustente a prova escrita, o enunciado formal precisa representar a mesma afirmação matemática. O resumo do preprint concentra sua crítica nesse vínculo entre as duas versões.
O que se sabe sobre a possível influência de trabalhos anteriores
A Scientific American relatou a suspeita de Buckmaster de que trabalhos anteriores dele e de Alpöge possam ter influenciado a OpenAI. Em 10 de setembro, a OpenAI afirmou que entradas de usuários posteriores a 3 de julho de 2026, incluindo o uso de Codex e ChatGPT por Buckmaster, não poderiam ter influenciado o modelo nem os resultados matemáticos.
O episódio se soma a outros debates sobre a produção matemática da empresa. A NeoTeo já abordou a retirada de três manuscritos da OpenAI após um erro de sinal.
