Cientistas encontram divergências na prova em Lean da OpenAI para Navier-Stokes

Cientistas compararam a prova publicada pela OpenAI sobre as equações de Navier-Stokes com sua versão formalizada em Lean e encontraram divergências em vários pontos-chave. Nesses trechos, a versão verificável por máquina prova afirmações mais fracas do que as declaradas no texto para humanos. As equações de Navier-Stokes integram a lista dos sete "problemas do milênio" do Instituto Clay de Matemática, e cada um deles tem prêmio de 1 milhão de dólares, de modo que qualquer rachadura em um resultado desse tipo chama atenção de imediato. Ainda assim, isso não é uma refutação.

O que exatamente foi encontrado

A verificação é simples. Toma-se o artigo com a prova e, em paralelo, a versão formal escrita em Lean, uma linguagem em que o computador confere cada passo do raciocínio. Se as duas versões descrevem a mesma coisa, elas coincidem. Aqui, não coincidiram: em alguns pontos centrais, a versão em Lean afirma menos do que o texto.

A descrição da verificação não diz se o trabalho da OpenAI pretende resolver por completo o problema do Clay ou chegar a um resultado mais específico. A dimensão da alegação deve ser avaliada pela própria publicação, e essa é uma ressalva importante. Mas ela não muda a conclusão: o artefato formal precisa corresponder ao que foi prometido no artigo.

Por que uma "afirmação mais fraca" é coisa séria

O Lean não aceita argumentos como "isso é óbvio" ou "decorre de considerações padrão". Se a prova passa na verificação, ela está correta em relação ao que de fato foi escrito na formalização. Por isso, a pergunta central é se a versão formal prova o mesmo que o texto afirma em palavras. Quando o enunciado no código é mais fraco do que o do artigo, há alguns cenários possíveis:

• os formalizadores simplificaram as condições para concluir o trabalho e não avisaram;
• o texto formula o teorema de modo impreciso, e a versão em Lean mostra o que de fato foi provado;
• um passo que no artigo parece provado não se sustenta numa verificação rigorosa;
• a divergência vem de uma incompatibilidade técnica de definições, que se resolve com um ajuste.

O primeiro e o quarto cenários são inofensivos; o terceiro é perigoso. Enquanto os autores ou especialistas independentes não analisarem cada ponto separadamente, não é possível escolher entre eles.

Principais fatos com base nos dados disponíveis:

• objeto da verificação: a prova da OpenAI sobre as equações de Navier-Stokes;
• método: comparação do texto publicado com a versão algorítmica em Lean;
• resultado: divergências em vários pontos-chave;
• natureza das divergências: na versão de máquina, as afirmações são mais fracas;
• situação: ainda não é uma refutação, mas é motivo para dúvida.

O que acompanhar daqui para frente

Para quem acompanha o uso de IA na matemática, vale ter alguns pontos de referência em mente. O primeiro é a reação da OpenAI. Uma análise clara de cada divergência, seja uma formulação corrigida, um código Lean atualizado ou o reconhecimento de limitações, dirá mais do que qualquer declaração genérica. O segundo é o que dirão os especialistas em dinâmica dos fluidos e em equações diferenciais parciais. A verificação formal confere a lógica, mas só matemáticos da área podem avaliar se o sentido do problema se perdeu pelo caminho. O terceiro é se a formalização e os materiais complementares serão publicados, para que a verificação possa ser reproduzida de forma independente.

Para quem toma decisões com base em alegações desse tipo, a conclusão é prática. Um resultado de IA em matemática só deve ser considerado confirmado quando houver verificação independente e a versão formal coincidir com o teorema declarado. Um comunicado de imprensa e um preprint não bastam para isso. Enquanto as divergências não forem resolvidas, a história de Navier-Stokes continua sendo uma alegação de peso, não um fato aceito.