Em 13 de outubro de 2026, a Scientific American relatou que grupos de especialistas passaram a considerar cada vez mais que o método do enxame final de agentes da OpenAI era distinto do programa dos matemáticos espanhóis Diego Córdoba e Luis Martínez-Zoroa. Em uma análise técnica separada, três pesquisadores apontaram uma diferença entre o artigo da OpenAI e a estimativa correspondente em Lean: quatro derivadas adicionais no texto e cinco na formalização examinada. A reportagem da Scientific American e a análise de Bastounis, Circelli e Hansen tratam de questões diferentes: o método do enxame e a correspondência entre a prova escrita e o código formal.
O que os especialistas dizem sobre o método da OpenAI
Segundo a Scientific American, especialistas que examinaram o trabalho avaliam cada vez mais que o grande enxame final seguiu um caminho distinto do programa associado a Diego Córdoba e Luis Martínez-Zoroa. A reportagem também registra que alguns especialistas consideram possível que um grupo preliminar menor tenha seguido esse programa para chegar a um resultado intermediário.
Essa distinção descreve o método atribuído ao grupo final e uma possível etapa anterior; não transforma a avaliação sobre o processo em um veredito sobre a prova matemática.
O que o Lean verifica — e o que a comparação com o artigo acrescenta
Lean é um assistente de provas: ele verifica uma demonstração formal em relação à afirmação codificada. Essa checagem, sozinha, não mostra que a afirmação formal reproduz fielmente o sentido de um artigo escrito em linguagem natural. É essa correspondência que Bastounis, Circelli e Hansen analisam ao comparar trechos do artigo da OpenAI com estimativas em Lean.
Lema 8.6: quatro derivadas no texto e cinco no Lean
No Lema 8.6, a afirmação em linguagem natural usa um limite com quatro derivadas adicionais de entrada; a estimativa Lean examinada pelos autores usa cinco. A diferença está nesse passo intermediário. Os autores não concluem que a prova da OpenAI em linguagem natural seja falsa.
| Versão examinada | Derivadas adicionais de entrada | Trecho |
| Artigo em linguagem natural | 4 | Lema 8.6 |
| Estimativa em Lean | 5 | Lema 8.6 |
Na estimativa do fluxo de pressão da equação (10.19), a expressão em linguagem natural usa B_R e se aplica a quase todo tempo. A estimativa Lean inclui A_R, usa termos diferentes e se aplica a todo tempo. Bastounis, Circelli e Hansen descrevem escolhas de prova distintas e dizem que é difícil comparar diretamente as duas formas.
O que a OpenAI afirma ter demonstrado
Em 8 de setembro de 2026, a OpenAI anunciou uma prova proposta para o problema de existência e regularidade de Navier–Stokes. A empresa afirma que seu resultado estabelece as afirmações C e D da formulação do Clay Mathematics Institute. Na construção descrita pela OpenAI, um fluido incompressível tridimensional, inicialmente suave e em repouso, sofre a ação de uma força externa suave e pode desenvolver uma singularidade em tempo finito, mantendo energia finita. O anúncio da OpenAI apresenta esse resultado como a alegação da empresa.
