Sobre o Problema do Prémio Millennium de Navier–Stokes

Partilhamos uma solução para o problema da existência e regularidade de Navier–Stokes, um dos Problemas do Prémio Millennium. Esta prova, produzida por um sistema interno da OpenAI, mostra que a dinâmica das equações de Navier–Stokes para o movimento de fluidos pode desenvolver uma singularidade em tempo finito. Partilhamos uma descrição da prova e uma formalização em Lean.

Os Problemas do Prémio Millennium⁠(abre numa nova janela) representam algumas das questões mais profundas da matemática de fronteira. A questão de saber se o movimento regular de um fluido tridimensional pode deixar de o ser permanece sem resposta há cerca de 90 anos.

Um dos principais objetivos do nosso trabalho é capacitar os cientistas para promoverem avanços na investigação e na tecnologia que beneficiem toda a humanidade. Para resolver o problema de Navier–Stokes, utilizámos um modelo interno significativamente mais capaz do que o GPT‑6 Astra. Consideramos importante informar o mundo sobre o ritmo do progresso da IA e o que esperar dos próximos modelos.

As equações de Navier–Stokes utilizam a segunda lei do movimento de Newton («F=ma») para descrever como se movem os fluidos. É importante salientar que tratam o fluido como um meio contínuo, em vez de acompanharem moléculas individuais. Estas equações são utilizadas na conceção de aeronaves, na previsão meteorológica e no estudo do fluxo sanguíneo.

Uma questão fundamental ainda em aberto sobre estas equações dinâmicas é saber se a aproximação do fluido como meio contínuo pode deixar de ser válida. Mais concretamente, podem as equações de Navier–Stokes para um fluido tridimensional incompressível de densidade constante desenvolver uma «singularidade», mesmo que o movimento comece de forma regular? Neste contexto, uma singularidade significa que a dinâmica leva as velocidades do fluido a crescerem sem limite num intervalo de tempo finito. O desenvolvimento de uma singularidade teria de ocorrer apesar da presença da viscosidade, que tende a suavizar o movimento. Como um fluido real não pode mover-se a uma velocidade infinita, isto assinalaria uma falha na forma como as equações modelam o fluido. Para continuar a modelar o sistema, seria então necessário acompanhar individualmente o comportamento de cada partícula.

As equações remontam ao trabalho de Claude-Louis Navier e George Gabriel Stokes no século XIX. Em 1934, Jean Leray provou que existem soluções num sentido generalizado, mas a questão de saber se permanecem sempre regulares tornou-se uma questão central sem resposta. Em 2000, o Clay Mathematics Institute incluiu o problema da existência e regularidade de Navier–Stokes entre os sete Problemas do Prémio Millennium.

O nosso sistema produziu uma prova analítica e uma formalização em Lean de que um fluido inicialmente regular e em repouso pode desenvolver uma singularidade em tempo finito. É aplicada ao fluido uma força regular, e a sua energia permanece finita ao longo de toda a dinâmica, desde o repouso até à formação da singularidade. Isto resolve o Problema do Prémio Millennium de Navier–Stokes ao estabelecer a afirmação «C» (e também a «D») na formulação oficial do Prémio Millennium⁠(abre numa nova janela).

A solução é um vórtice, um remoinho de fluido em rotação, que descreve uma espiral para o interior e fica cada vez mais alongado, como esparguete. Esta região central contrai-se à medida que acelera, de tal forma que a sua energia continua finita, conforme exigido pelas leis da física. O desafio técnico consiste em fazer com que as equações desenvolvam a falha através do movimento do próprio fluido, em vez de, por exemplo, introduzirmos manualmente uma força infinita. Em termos mais matemáticos, os termos das equações de Navier–Stokes que descrevem o movimento — aceleração, gradientes de pressão, transferência de quantidade de movimento e viscosidade — têm de se tornar grandes e, ainda assim, anular-se de forma precisa. Este equilíbrio pormenorizado mantém regular a força externa, mesmo quando a velocidade do fluido cresce sem limite.

Desde 28 de agosto, temos vindo a treinar um novo modelo interno que demonstrou um desempenho sem precedentes nas nossas avaliações de referência, incluindo em matemática. O treino deste modelo continua, tal como a melhoria do seu desempenho.

Na terça-feira, 1 de setembro, ouvimos rumores de que dois problemas do Prémio Millennium tinham sido resolvidos. Inspirados por estes rumores e pelo salto de desempenho do nosso modelo interno, iniciámos um esforço para o avaliar em todos os problemas do Prémio Millennium ainda em aberto e noutros problemas de grande impacto.

Utilizámos um sistema de agentes coordenados, assente no nosso modelo interno. Os agentes tinham acesso a ferramentas que lhes permitiam, por exemplo, consultar uma versão da Internet em cache e executar código. Os agentes foram divididos em grupos, com capacidade para comunicarem entre si dentro de cada grupo. Os grupos tinham dimensões variadas, e o grupo que produziu a resolução de Navier–Stokes envolveu cerca de 10 000 agentes em simultâneo. Mantivemos sempre as mesmas salvaguardas rigorosas que aplicamos a todas as avaliações dos nossos modelos de fronteira, incluindo monitorização e isolamento.

Para cada problema, apresentámos a diferentes grupos de agentes variantes distintas do enunciado, abrangendo todas as variantes do problema. No caso de Navier–Stokes, propusemos as versões «A» e «B» (formas específicas do problema que resultariam numa prova) e as versões «C» e «D» (que resultariam numa refutação) a grupos distintos de agentes.

Além dos problemas do Prémio Millennium completos, pedimos ao nosso sistema multiagente que tentasse resolver um conjunto de problemas «mais fáceis». Um deles era uma questão semelhante sobre a formação de singularidades no limite do problema de Navier–Stokes em que se remove o termo da viscosidade. Esta questão é conhecida como o problema da regularidade das equações de Euler, e os nossos agentes surpreenderam-nos ao resolvê-la. A variante específica que resolveram foi a versão sem força externa, na qual não é aplicada qualquer força externa ao fluido. Quase 100 agentes trabalharam em conjunto durante cerca de 50 horas para produzirem a nossa refutação da regularidade de Euler¹.

Quando vimos a solução de Euler, considerámos que Navier–Stokes era o problema mais promissor em que trabalhar. Decidimos, por isso, dedicar os nossos recursos a Navier–Stokes. Para tal, retirámos agentes dos outros Problemas do Prémio Millennium e enviámos prompts com a resolução de Euler. Quando ficou disponível uma versão do nosso modelo interno com treino adicional, atualizámos os agentes para esse modelo.

Incentivámos diferentes grupos de agentes a explorar uma diversidade de abordagens. Após algum tempo, promovemos a troca de ideias entre os grupos de agentes, utilizando o Codex para consolidar as conclusões mais úteis de cada grupo. Estes prompts de seguimento basearam-se nos resultados intermédios dos próprios agentes. O grupo que encontrou a solução para Navier–Stokes foi orientado desta forma.

Os agentes chegaram à resolução no sábado, 5 de setembro, cerca de 88 horas após a entrada em funcionamento dos primeiros agentes. A formalização e verificação em Lean demoraram mais 17 horas através do GPT‑6 Astra.

No conjunto de todos os problemas tentados, os agentes enviaram 4,9 milhões de mensagens e utilizaram cerca de 300 mil milhões de tokens de saída. Durante a resolução do problema de Navier–Stokes, os agentes enviaram 2,7 milhões de mensagens e utilizaram aproximadamente 130 mil milhões de tokens de saída.

O nosso esforço começou a 1 de setembro, depois de ouvirmos um rumor que mais tarde percebemos estar relacionado com Levent Alpöge, funcionário da Anthropic, e Tristan Buckmaster, professor de matemática na NYU.² Após concluirmos todo o projeto e a verificação em Lean (a 6 de setembro), e acreditando, com base no rumor, que também tinham uma solução para Navier–Stokes, contactámo-los para propor a publicação simultânea do nosso resultado e reconhecer a prioridade do seu trabalho num anúncio conjunto. Foi então que soubemos que, utilizando um modelo interno da Anthropic, tinham produzido uma resolução do problema de Euler com força externa. Nessas conversas, oferecemo-nos para lhes dar acesso a todos os prompts que utilizámos e, posteriormente, à prova. Reconhecemos a prioridade do seu trabalho sobre Euler com força externa e felicitamo-los pela notável conquista matemática.

Nós (os investigadores e os agentes) não tivemos acesso, por qualquer meio, a nenhum dos seus trabalhos antes da publicação — em particular, não foram consultados dados específicos de utilizadores para resolver este problema.

Após uma investigação, confirmámos que os prompts de Buckmaster ao Codex nos dois meses anteriores a este anúncio e ao artigo de 8 de setembro de 2026 não poderiam ter influenciado o sistema de forma alguma, nem mesmo através do treino. O modelo interno da OpenAI utilizado neste resultado foi desenvolvido através de aprendizagem por reforço em grande escala, com base num modelo previamente pré-treinado. As nossas provas também são significativamente diferentes. No caso de Euler, Alpöge e Buckmaster provaram um resultado com força externa, enquanto o sistema da OpenAI provou um resultado sem força externa.

Ao publicar este resultado, pretendemos dar conta do progresso substancial dos nossos modelos de IA. Não tencionamos candidatar este resultado ao Prémio Millennium.

Este marco representa um trabalho substancial de matemáticos e investigadores de IA. Contudo, isto não representa o culminar do desenvolvimento da IA, mas antes um retrato do seu progresso num determinado momento.

Acreditamos ter entrado numa nova fase do progresso da IA⁠, e os resultados de hoje constituem mais uma prova disso. Estamos concentrados em compreender este modelo e em utilizar o que aprendemos para orientar e definir o ritmo dos próximos avanços nas suas capacidades. Um dos nossos principais objetivos⁠ é criar sistemas de IA orientáveis, responsáveis e ligados às pessoas, o que poderá exigir escolhas mais ponderadas sobre o ritmo do progresso, à medida que prosseguimos a nossa missão de garantir que a AGI beneficia toda a humanidade.