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

Estamos compartilhando uma solução para o problema de existência e suavidade de Navier–Stokes, um dos Problemas do Prêmio Millennium. Essa 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. Estamos compartilhando tanto uma exposição da prova quanto sua formalização em Lean.

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

Um dos principais objetivos do nosso trabalho é capacitar cientistas a promover avanços em pesquisa e tecnologia que beneficiem toda a humanidade. Para resolver o problema de Navier–Stokes, usamos um modelo interno significativamente mais capaz que o GPT‑6 Astra. Acreditamos que é 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 usam a segunda lei do movimento de Newton ("F=ma") para descrever como os fluidos se movem. É importante destacar que elas tratam o fluido como um meio contínuo, em vez de acompanhar moléculas individuais. Essas equações são usadas no projeto de aeronaves, na previsão do tempo e no estudo do fluxo sanguíneo.

Uma questão fundamental em aberto sobre essas equações dinâmicas é se a aproximação contínua do fluido pode deixar de ser válida. Especificamente, as equações de Navier–Stokes para um fluido tridimensional incompressível de densidade constante podem desenvolver uma "singularidade", mesmo quando o movimento começa de forma suave? Aqui, uma singularidade significa que a dinâmica faz as velocidades do fluido crescerem sem limite em um 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 se mover a uma velocidade infinita, isso indicaria uma falha na forma como as equações modelam o fluido. Para continuar modelando 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 em um sentido generalizado, mas saber se elas sempre permanecem suaves tornou-se uma questão central ainda sem resposta. Em 2000, o Clay Mathematics Institute incluiu o problema de existência e suavidade de Navier–Stokes entre os sete Problemas do Prêmio Millennium.

Nosso sistema produziu uma prova analítica e uma formalização em Lean de que um fluido inicialmente suave e em repouso pode desenvolver uma singularidade em tempo finito. Uma força suave é aplicada ao fluido, e sua energia permanece finita durante toda a dinâmica, desde o repouso até a formação da singularidade. Isso 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 em uma nova janela).

A solução é um vórtice — um redemoinho de fluido em rotação — que espirala para dentro e se alonga cada vez mais, como espaguete. Essa região central encolhe enquanto acelera, de modo que sua energia continua finita, conforme exigido pelas leis da física. O desafio técnico é fazer com que as equações desenvolvam essa falha por meio do próprio movimento do fluido, e não, por exemplo, pela introdução artificial de 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 momento e viscosidade — precisam se tornar grandes e, ao mesmo tempo, se cancelar de maneira precisa. Esse equilíbrio minucioso mantém a força externa suave, mesmo quando a velocidade do fluido cresce sem limite.

Desde 28 de agosto, estamos treinando um novo modelo interno que apresentou desempenho sem precedentes em nossas avaliações, inclusive em matemática. O treinamento desse modelo continua, e seu desempenho segue melhorando.

Na terça-feira, 1º de setembro, ouvimos rumores de que dois Problemas do Prêmio Millennium haviam sido resolvidos. Inspirados por esses rumores e pelo salto de desempenho do nosso modelo interno, iniciamos um esforço para avaliá-lo em todos os Problemas do Prêmio Millennium ainda em aberto e em alguns outros problemas de alto impacto.

Usamos um sistema de agentes coordenados, baseado em nosso modelo interno. Os agentes tinham acesso a ferramentas, como a capacidade de consultar uma versão armazenada em cache da internet e executar código. Os agentes foram subdivididos em grupos, com a capacidade de se comunicar dentro de cada grupo. Os grupos variavam de tamanho, e aquele que produziu a solução de Navier–Stokes envolveu cerca de 10 mil agentes simultâneos. Mantivemos em todos os momentos as mesmas salvaguardas rigorosas aplicadas a todas as avaliações de nossos modelos de fronteira, incluindo monitoramento e isolamento.

Para cada problema, apresentamos a diferentes grupos de agentes variantes distintas do enunciado, abrangendo todas as versões do problema. No problema de Navier–Stokes, sugerimos as versões "A" e "B" (formas específicas do problema que resultariam em uma prova) e as versões "C" e "D" (que resultariam em uma 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 sem o termo de viscosidade. Isso é conhecido como o problema de regularidade das equações de Euler, e nossos agentes nos surpreenderam ao resolver essa questão. A variante específica que eles resolveram foi a versão sem força externa, na qual nenhuma força externa é aplicada ao fluido. Quase 100 agentes trabalharam juntos por aproximadamente 50 horas para produzir nossa refutação da regularidade de Euler¹.

Quando vimos a solução de Euler, consideramos Navier–Stokes o problema mais promissor a explorar. Por isso, decidimos dedicar nossos recursos a Navier–Stokes. Para isso, transferimos agentes dos outros Problemas do Millennium e apresentamos a eles a solução de Euler. Quando uma versão mais treinada do nosso modelo interno ficou disponível durante o trabalho, atualizamos nossos agentes para esse modelo.

Incentivamos diferentes grupos de agentes a explorar uma variedade de abordagens. Depois de algum tempo, promovemos a troca de ideias entre os grupos de agentes usando o Codex para consolidar as contribuições mais úteis de cada grupo. Essas instruções de acompanhamento aproveitaram os próprios resultados intermediários dos agentes. O grupo que encontrou a solução de Navier–Stokes foi orientado dessa maneira.

Os agentes chegaram à solução no sábado, 5 de setembro, cerca de 88 horas após o lançamento dos primeiros agentes. A formalização e a verificação em Lean exigiram mais 17 horas com o GPT‑6 Astra.

Considerando todos os problemas abordados, os agentes enviaram 4,9 milhões de mensagens e usaram cerca de 300 bilhõ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 usaram aproximadamente 130 bilhões de tokens de saída.

Nosso trabalho começou em 1º de setembro, após ouvirmos um rumor que depois percebemos estar relacionado a Levent Alpöge, funcionário da Anthropic, e Tristan Buckmaster, professor de matemática da NYU.² Após concluirmos todo o projeto e a verificação em Lean (em 6 de setembro), e acreditando pelo rumor que eles também tinham uma solução para Navier–Stokes, entramos em contato para propor a divulgação simultânea do nosso resultado e reconhecer a prioridade deles em um anúncio conjunto. Nesse momento, descobrimos que eles haviam produzido, usando um modelo interno da Anthropic, uma solução para o problema de Euler com força externa. Nessas conversas, oferecemos a eles acesso a todas as instruções que usamos e, posteriormente, à prova. Reconhecemos a prioridade do trabalho deles sobre Euler com força externa e os parabenizamos por essa notável conquista matemática.

Nós — pesquisadores e agentes — não tivemos acesso ao trabalho deles por nenhum meio até sua divulgação pública. Em particular, nenhum dado específico de usuário foi acessado para resolver esse problema.

Após uma investigação, confirmamos que as instruções 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 nenhuma forma, nem mesmo por meio do treinamento. O modelo interno da OpenAI usado para esse resultado foi desenvolvido por meio de aprendizado por reforço em grande escala, aplicado sobre um modelo previamente pré-treinado. Nossas provas também diferem significativamente. 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.

Nosso objetivo ao divulgar esse resultado é comunicar o avanço substancial de nossos modelos de IA. Não pretendemos reivindicar o Prêmio Millennium por esse resultado.

Esse marco representa um trabalho substancial de matemáticos e pesquisadores de IA. No entanto, isso não é o ponto culminante, mas um retrato momentâneo do progresso no desenvolvimento da IA.

Acreditamos que entramos em uma nova fase do progresso da IA⁠, e os resultados de hoje oferecem mais evidências disso. Estamos concentrados em compreender esse modelo e usar o que aprendermos para orientar e definir o ritmo da busca por novos avanços de capacidade. Um de nossos principais objetivos⁠ é criar sistemas de IA que possam ser orientados, sejam responsáveis e estejam conectados às pessoas. Isso pode exigir escolhas mais deliberadas sobre o ritmo do progresso enquanto seguimos nossa missão de garantir que a AGI beneficie toda a humanidade.