A verificação formal na linguagem Lean é um dos principais elementos da proposta apresentada por matemáticos da OpenAI para as equações de Navier-Stokes. O resultado ainda precisa passar pelo exame da comunidade científica, mas pode resolver um dos seis Problemas do Milênio que continuam em aberto.
A demonstração contou com 10 mil agentes autônomos de inteligência artificial e se baseia em uma estratégia criada pelos pesquisadores Diego Córdoba e Luis Martínez-Zoroa. A ideia usa uma sequência infinita de camadas, cada uma correspondente a uma solução regular. Reunidas em uma espécie de cascata, elas podem formar uma nova solução que desenvolve uma singularidade.
O papel da viscosidade
As equações de Navier-Stokes foram formuladas no século 19 para aplicar a segunda lei de Newton ao movimento dos fluidos. Elas são usadas para descrever fenômenos como correntes oceânicas e o deslocamento do ar. A questão central é saber se suas soluções permanecem regulares ou se podem evoluir até uma região infinitamente pequena atingir velocidade ilimitada.
Esse possível comportamento é chamado de blowup, ou explosão da solução. A conclusão não indica que água, ar ou outro fluido real possa alcançar velocidade infinita. O modelo considera a matéria um meio contínuo, divisível indefinidamente, enquanto os fluidos são formados por moléculas e átomos.
O problema do Clay Mathematics Institute considera um espaço tridimensional ilimitado e forças externas matematicamente suaves. A viscosidade também faz parte da questão: ao contrário das equações de Euler, que representam fluidos sem atrito, Navier-Stokes inclui a resistência interna presente em materiais como água e mel.
De Euler à nova construção
Córdoba afirmou que, dez anos atrás, a possibilidade de uma singularidade nas equações de Navier-Stokes era considerada improvável: “Dez anos atrás, ninguém acreditava que houvesse uma singularidade para Navier-Stokes”. A mudança de perspectiva foi influenciada por pesquisas sobre as equações de Euler, incluindo um estudo publicado em 2019 sobre a formação de singularidades.
Em 2023, Córdoba e Martínez-Zoroa demonstraram que uma versão das equações de Euler, submetida a uma força externa menos regular, podia desenvolver singularidades. Esse trabalho forneceu parte da base para a estratégia aplicada agora ao sistema com viscosidade. Os agentes de IA ampliaram a abordagem para atender às condições específicas de Navier-Stokes, sem fronteiras e com uma força suave.
O anúncio foi feito nesta terça-feira (8), apenas 12 horas depois de Tristan Buckmaster, da Universidade de Nova York, e Levent Alpöge, da Anthropic, divulgarem resultados relacionados obtidos com outros modelos de IA. A proximidade provocou discussões sobre prioridade e crédito científico.
Charles Fefferman, matemático de Princeton responsável pela descrição oficial do problema, apontou Córdoba e Martínez-Zoroa como os protagonistas intelectuais. A formalização em Lean fornece evidência de correção, mas a proposta ainda terá de ser submetida a novas análises.
