Agentes de IA reivindicam Navier-Stokes e matemáticos reagem

A OpenAI diz que 10.000 de seus agentes de IA resolveram um problema em que os matemáticos trabalham há um século. Três dias depois, 25 ganhadores da maior honraria da matemática assinaram uma declaração que alerta exatamente contra esse tipo de anúncio. As duas coisas aconteceram na mesma semana, e a distância entre elas é a história.

Navier-Stokes é um conjunto de equações que descreve como os fluidos se movem. A questão em aberto, que vale um milhão de dólares, era se as soluções em três dimensões sempre continuam suaves ou podem explodir. A Quanta Magazine noticiou em 8 de setembro que os agentes da OpenAI encontraram essa explosão, chamada de singularidade.

O que os agentes produziram

A Quanta apresenta números que dizem tanto sobre o método quanto sobre o resultado.

Medida	Número
Agentes em execução	10.000, autônomos
Tempo até a prova	88 horas
Tempo para formalizá-la	Mais 17 horas
Mensagens trocadas entre os agentes	Quase 5 milhões
Custo estimado de computação	Vários milhões de dólares

Formalizar uma prova significa reescrevê-la para que um computador possa verificar cada passo de forma mecânica. É a parte que permite a quem está de fora confiar em um resultado sem acompanhar o argumento por conta própria. Nossa reportagem anterior sobre a IA da Anthropic formalizando o último teorema de Fermat tratou da mesma técnica aplicada a um resultado muito mais antigo.

O crédito não está bem repartido, e a Quanta diz isso. Tristan Buckmaster e Levent Alpöge anunciaram doze horas antes um resultado relacionado sobre as equações de Euler, também com ajuda de IA. A Quanta relata uma disputa sobre a cronologia e sobre o acesso a trabalhos anteriores aos anúncios. Ela também aponta as técnicas analíticas de Diego Córdoba e Luis Martínez-Zoroa como essenciais para os dois esforços.

O que o Clay Institute realmente disse

O Clay Mathematics Institute definiu os Millennium Prize Problems no ano 2000, cada um valendo um milhão de dólares. A Quanta conta seis que ainda estavam em aberto antes dessa afirmação. É o órgão que decide se algum deles foi resolvido.

O comunicado de 11 de setembro tem três palavras cuidadosas na parte que importa. O problema "aparentemente foi resolvido". O instituto acrescentou que sua avaliação segue regras estabelecidas e é deliberadamente sem pressa.

Ninguém foi pago. "Aparentemente resolvido" é o reconhecimento de que existe uma afirmação e de que ela parece séria, não uma decisão de que ela está correta.

Por que 25 matemáticos assinaram um alerta

No mesmo dia, Terence Tao publicou um texto sobre uma declaração conjunta de 25 laureados com a Fields Medal. A Fields Medal é o equivalente ao prêmio Nobel na matemática.

A objeção deles não é que os resultados de IA estejam errados. É que as empresas de IA tratam problemas matemáticos como testes de desempenho, e que os resultados chegam anunciados depressa, sem um texto completo nem citações. Isso conflita com o modo como a matemática costuma funcionar, em que o entendimento é construído por uma longa troca entre pessoas.

A formulação de Tao é a linha mais afiada do texto. Ele escreve que "resolver problemas é apenas uma ferramenta e um indicador indireto para alcançar o objetivo principal, que é o entendimento conceitual". A declaração alerta que "a produção em massa, em ritmo cada vez mais rápido, de enunciados 'verdadeiro/falso' pode destruir terreno fértil", e que o que está em risco é a cadeia de transmissão entre matemáticos.

O que isto significa para programadores

Você é o público desses anúncios, então leia-os como um revisor leria. Faça três perguntas a qualquer resultado de IA que vir neste ano. Existe um texto que você poderia conferir. Ele foi verificado formalmente, e contra o quê. Quem mais estava trabalhando nisso, e essas pessoas foram creditadas.

Separe a verificação do entendimento, porque não são a mesma garantia. Uma prova verificada por máquina diz a você que os passos se encaixam. Ela não diz nada sobre por que o resultado é verdadeiro nem sobre até onde ele se generaliza. Se você encaixa uma saída de IA formalmente verificada no seu próprio trabalho, importou um fato que ainda não sabe explicar, e isso tem um custo quando ele quebra.

Desconte especificamente o enquadramento de benchmark. A queixa dos laureados com a Fields Medal é que problemas resolvidos estão sendo usados como placares, e um placar premia quem anuncia primeiro. O relato da Quanta sobre uma diferença de doze horas e uma cronologia contestada é o que esse incentivo produz. A mesma pressão está por trás dos números de benchmark de modelos que você lê na hora de escolher uma API.

A lição de engenharia é a mais barata de levar. Dez mil agentes, cinco milhões de mensagens e 88 horas produziram algo real aqui, e o artefato que tornou isso verificável foi a formalização, não os agentes. Se você constrói sistemas multiagente, a parte transponível é que a saída precisa de uma verificação mecânica no final. Sem ela, você tem uma resposta confiante e nenhuma maneira de auditá-la.