“Quando provar fica barato, compreender fica mais valioso”
Em 2000, o Clay Mathematics Institute estabeleceu sete Problemas do Milênio, escolhidos entre algumas das questões mais profundas da matemática. Um deles, a conjectura de Poincaré, foi posteriormente resolvido por Grigori Perelman.
Agora surgiu um episódio que merece atenção, mas também precisão. As equações de Navier–Stokes descrevem o movimento de fluidos, como água e ar, e são utilizadas em inúmeras aplicações científicas e de engenharia. Mas existe uma questão matemática profunda no caso tridimensional: partindo de condições suficientemente regulares, as soluções permanecem regulares indefinidamente ou podem desenvolver uma singularidade em tempo finito?
O Problema do Milênio admite caminhos diferentes para sua resolução. Simplificando bastante, pode-se provar a existência e regularidade global das soluções nas condições especificadas ou demonstrar, por meio de um exemplo admissível, que essa regularidade pode falhar. As alternativas C e D da formulação oficial pertencem a essa segunda possibilidade e envolvem versões com força externa.
É aqui que entra o resultado anunciado pela OpenAI. Segundo a empresa, um sistema de agentes baseado em um modelo interno ainda não disponibilizado publicamente explorou diferentes abordagens para o problema. O grupo que produziu a resolução chegou a envolver aproximadamente 10 mil agentes concorrentes.
“10 mil agentes” não significa 10 mil modelos diferentes nem 10 mil matemáticos artificiais independentes. Eram muitas instâncias de um sistema baseado no mesmo modelo interno, organizadas em grupos, explorando abordagens diferentes e compartilhando resultados. Ferramentas também foram utilizadas, incluindo execução de código e acesso a uma versão armazenada da internet.
Cerca de 88 horas depois do início do esforço, os agentes chegaram a uma construção que, segundo a OpenAI, demonstra que um fluido inicialmente regular e em repouso, submetido a uma força externa suave, pode desenvolver uma singularidade em tempo finito, mantendo energia finita durante a evolução.
A empresa afirma que isso estabelece as alternativas C e D da formulação oficial do Problema do Milênio.
Portanto, não estamos falando simplesmente de alguém ter perguntado ao ChatGPT como resolver Navier–Stokes. Trata-se de um sistema computacional de pesquisa em larga escala, baseado em um modelo interno mais capaz que o GPT-6 Astra e utilizando enorme quantidade de inferência paralela.
Depois veio uma segunda etapa. A demonstração analítica precisava ser examinada e também poderia ser traduzida para uma linguagem formal, na qual cada passo pudesse ser verificado mecanicamente.
Foi utilizado o Lean, um proof assistant que permite representar definições, hipóteses e inferências em linguagem matemática formal. Segundo a OpenAI, a formalização e sua verificação levaram aproximadamente mais 17 horas e utilizaram o GPT-6 Astra.
Isso acrescenta uma camada importante de confiança: o sistema verifica mecanicamente se a derivação formal segue das definições, hipóteses e regras codificadas.
Mas isso não elimina uma terceira etapa: o escrutínio da comunidade matemática. Uma formalização pode ser internamente válida e ainda ser necessário verificar se suas definições e hipóteses representam corretamente o problema matemático original, além de compreender o significado, a originalidade e o alcance do resultado.
Essa distinção ficou ainda mais interessante porque o próprio Clay Mathematics Institute se manifestou após o anúncio. O instituto afirmou que o problema aparentemente foi resolvido, mas ressaltou que a avaliação do resultado e a atribuição de crédito seguirão o processo formal previsto pelas regras do Millennium Prize. E a própria OpenAI declarou que não pretende reivindicar o prêmio.
Portanto, eu evitaria tanto minimizar quanto exagerar o episódio. Não é apenas “um LLM↳LLMs48 conteúdosConsiderações básicas de hardware para modelos de linguagem em código aberto: Memória, Desempenho e ViabilidadeMarketing Tech · out 2025Modelos de linguagem sob ataque: o lado obscuro da IA generativaDevSecOps · mai 2025Criando um LLM – modelo de linguagem de grande escala – do zero com TransformersAI · abr 2024Ver tudo em AI → respondeu corretamente a um problema difícil”. Mas também é cedo para transformar o anúncio em uma narrativa de que a IA automatizou a matemática.
O que temos é um sistema de IA que produziu uma demonstração analítica, posteriormente formalizada e verificada em Lean, para um resultado que a OpenAI afirma resolver as alternativas C e D da formulação oficial e que o Clay Mathematics Institute considera, neste momento, aparentemente resolvido.
Isso, por si só, já é extraordinário. Mas talvez a consequência mais interessante venha depois. Podemos estar caminhando para uma era de maior abundância de provas matemáticas. E aqui existe uma distinção fundamental. Provar não é o mesmo que descobrir.
Uma prova estabelece uma proposição por meio de uma cadeia válida de inferências dentro de determinado sistema matemático. Descoberta matemática é um processo mais amplo: envolve escolher problemas relevantes, formular conjecturas, perceber conexões inesperadas, criar conceitos, desenvolver métodos e reconhecer por que determinado resultado importa.
A história da matemática não avançou apenas porque matemáticos provaram teoremas. Avançou também porque criaram novas maneiras de formular problemas e enxergar estruturas que antes não eram percebidas.
Por isso, mesmo que sistemas de IA venham a produzir milhares de provas, não decorre daí que estejam produzindo milhares de descobertas matemáticas relevantes.
Há ainda outra dimensão. O processo de tentar, errar, abandonar caminhos, reformular hipóteses e desenvolver ferramentas também produz conhecimento. Um matemático pode trabalhar anos em um problema sem resolvê-lo e, ainda assim, transformar seu campo pelos conceitos e métodos desenvolvidos durante a investigação. A solução final não contém necessariamente todo o conhecimento produzido no caminho.
E isso vai muito além da matemática. Um estudante pode entregar uma resposta melhor sem aprender mais. Um desenvolvedor pode produzir muito mais código sem compreender melhor o sistema. Um executivo pode gerar análises sofisticadas sem desenvolver proporcionalmente sua capacidade de julgamento.
Produção intelectual e desenvolvimento intelectual não são a mesma coisa. Se sistemas de IA passarem a gerar provas em grande escala, o gargalo pode migrar. Em vez de apenas produzir resultados, precisaremos selecionar quais importam, verificar sua validade, estabelecer conexões, interpretar seu significado e decidir quais merecem orientar novas linhas de pesquisa.
Também podemos usar IA nessas tarefas. IA propõe. IA formaliza. IA verifica. IA seleciona. IA explica. Mas seria precipitado concluir que isso automatiza a descoberta matemática como um todo.
O resultado de Navier–Stokes fornece uma evidência extraordinária de que partes importantes da pesquisa matemática podem ser aceleradas e, em alguns casos, realizadas por sistemas de IA. Ainda não sabemos quão amplamente essa capacidade se generalizará.
Não defendo preservar dificuldades artificialmente nem impedir máquinas de resolver problemas. Seria absurdo transformar a dificuldade em objetivo. O ponto é outro. Se a produção de provas se tornar progressivamente mais barata e abundante, outras capacidades podem ganhar ainda mais importância: formular boas perguntas, reconhecer relevância, criar conceitos, estabelecer conexões e compreender o significado dos resultados.
A IA pode tornar provas cada vez mais abundantes. Mas abundância de provas não significa abundância de descobertas. E nenhuma das duas garante abundância de compreensão.
Podemos acabar sabendo coletivamente muito mais matemática sem que isso signifique, necessariamente, que cada um de nós esteja compreendendo muito mais matemática.
O link da publicação da OpenAI: https://openai.com/index/navier-stokes-solution/?utm_source=chatgpt.com
E o da Clay Mathematics Institute: https://www.claymath.org/news/navier-stokes-announcement/?utm_source=chatgpt.com . Observem que o comunicado da Clay não celebra apenas a obtenção da prova. O Clay destaca que os Problemas do Milênio foram concebidos para estimular o desenvolvimento de novas estruturas, métodos e compreensão matemática, e diz esperar que a análise das inovações por trás desse resultado produza novas ondas de compreensão humana. Isso reforça diretamente a distinção entre prova, descoberta e compreensão.
É CEO da Litteris Consulting. Profissional e estudioso de Tecnologia da Informação desde fins da década de 70, com educação formal diversificada, em Economia, mestrado em Ciência da Computação e MBA em Marketing de Serviços, e experiência profissional moldada pela passagem em empresas de porte mundial. Escreve constantemente sobre tecnologia da informação em publicações especializadas como CIO Magazine, Mundo Java, além do iMasters, e apresenta palestras em eventos e conferências de renome. É autor de sete livros que abordam assuntos como Software Livre, Grid Computing, Software Embarcado, Cloud Computing e Big data.
