OpenAI diz ter uma prova gerada por IA para o problema de Navier-Stokes, e verificá-la é difícil

Há um mês, a OpenAI anunciou ter obtido uma prova gerada por IA para o problema de Navier-Stokes. Ele é um dos sete "Problemas do Milênio": o Clay Mathematics Institute promete US$ 1 milhão por cada solução, e desde 2000 apenas um deles foi resolvido, a conjectura de Poincaré. Agora, o Bloomberg Tech dedicou ao tema um episódio com Justin Solomon, vice-decano de educação em engenharia do MIT. Uma ressalva importante: o material é o anúncio de um podcast, não uma análise da prova em si. Ele não traz confirmação de que a prova está correta.

Que problema é esse e por que é tão difícil verificá-lo?

As equações de Navier-Stokes descrevem o movimento de fluidos viscosos: a água em um cano, o ar sobre a asa de um avião, as correntes na atmosfera. Engenheiros e climatologistas as resolvem numericamente todos os dias. Mas os matemáticos ainda não provaram que, em três dimensões, essas equações sempre têm uma solução suave que não "explode" em tempo finito. A prática funciona, mas falta uma teoria rigorosa.

Segundo a descrição do episódio, Solomon explica tanto o enunciado do problema quanto o motivo de o texto da OpenAI ser difícil de ler até para profissionais. Para a matemática, esse ponto é fundamental. Uma prova só é considerada prova depois de verificada pela comunidade. Se um texto de centenas de páginas foi escrito por um modelo e está cheio de passos pouco familiares, a verificação pode levar meses. Nenhum comunicado de imprensa acelera esse processo.

Modelos que antes não sabiam fazer contas

O material traz um detalhe que ajuda a dimensionar a mudança: os modelos de linguagem já erraram em aritmética elementar e agora resolvem problemas que ficaram em aberto por décadas. Solomon analisa como matemáticos puros e aplicados reagem a isso. Os interesses de cada grupo são diferentes. Para os aplicados, importam mais uma ferramenta que funcione e um resultado numérico. Os puros querem compreensão, ou seja, uma estrutura de argumento que possa ser transmitida a outra pessoa.

Outro tema do episódio é como o cinema retrata o trabalho dos matemáticos. Em geral, aparece um gênio diante de um quadro-negro, com uma epifania no meio da noite. O trabalho real consiste em longas verificações, becos sem saída e troca de mensagens com colegas.

Principais fatos do anúncio

• Anúncio: em setembro de 2026, a OpenAI declarou ter uma prova gerada por IA para o problema de Navier-Stokes. • Status: a fonte não menciona verificação independente. • O que está em jogo: o prêmio do Clay Mathematics Institute pela solução de um Problema do Milênio é de US$ 1 milhão. • Especialista: Justin Solomon, associate dean for engineering education no MIT. • Problema: até profissionais têm dificuldade para destrinchar o texto da prova. • Frente paralela: LLMs fazem lições de casa de estudantes, e os professores não conseguem se adaptar a tempo.

O que fazer: professores e engenheiros

A educação enfrentou o problema antes da ciência. Se o modelo resolve a lição de casa padrão, o que se deve avaliar não é a resposta, mas o raciocínio: defesas orais, questões com explicação, provas sem dispositivos. Segundo a descrição, Solomon já está revendo sua própria abordagem pedagógica, mas o anúncio não dá detalhes.

Para as equipes de engenharia, a conclusão é mais pé no chão. Qualquer resultado de um modelo em matemática, de otimização a simulação de escoamentos, precisa ser verificado de forma independente: com sistemas formais de prova, testes numéricos ou um segundo especialista. Enquanto a comunidade não confirmar o trabalho da OpenAI, ele deve ser tratado como uma alegação. Se for confirmado, os matemáticos ganharão uma nova classe de ferramentas e um novo problema: como ler provas que os próprios humanos não teriam concebido.