O que a Anthropic revelou de facto

Em 10 de agosto de 2026, a Anthropic publicou uma nota de investigação a descrever o que aconteceu quando apontou uma versão de investigação da Claude, ainda não lançada, para a hipótese de Riemann, a conjetura de 1859 segundo a qual todos os zeros não triviais da função zeta de Riemann têm parte real igual a um meio. A Claude não provou a hipótese. Fez avançar uma questão mais restrita e em aberto há décadas: que fração desses zeros os matemáticos conseguem provar rigorosamente que se situam nessa linha crítica. O recorde anterior, detido desde 2020 por Kyle Pratt, Nicolas Robles, Alexandru Zaharescu e Dirk Zeindler, situava essa fração comprovável em 41,6 por cento.

A execução de investigação da Claude elevou essa fração para 67,2 por cento, um resultado que, segundo a Anthropic, foi na realidade um subproduto de uma tentativa mais ampla de resolver a hipótese completa, e não o objetivo original. A empresa enquadra o número com cautela: trata-se de um resultado sobre um limite inferior, aplicado a um subproblema específico e bem definido, e não de um passo que resolve, ou se espera que venha a resolver, a conjetura com 167 anos.

Dentro do enxame de 60 agentes

A mecânica é a parte mais invulgar desta história. A trabalhar dentro do Claude Code ao longo de duas sessões, o modelo passou cerca de um dia e meio, na ordem das 36 horas, a coordenar cerca de 60 subagentes da Claude. Consumiu 31 milhões de tokens de saída e emitiu cerca de 2400 comandos de shell. Dos 60 agentes, apenas 2 desenvolveram a ideia matemática que acabou por resultar; 13 contribuíram com peças de apoio a essa ideia; 30 tentaram abordagens alternativas e falharam; e 13 atuaram como validadores, a verificar o trabalho em vez de o gerar. Antes de chegar à linha de ataque bem-sucedida, o enxame já tinha experimentado e descartado cerca de 650 ideias anteriores.

A intuição que desbloqueou o problema foi tratar os zeros, tanto os que estão sobre a linha crítica como os que estão fora dela, como pontos de um único espaço geométrico unificado, em vez de analisar os dois casos em separado, o que produziu uma desigualdade subjacente mais forte. A abordagem baseou-se em trabalho publicado pelos matemáticos Baluyot, Goldston, Suriajaya e Turnage-Butterbaugh, combinado com um artigo de 2000 de Enrico Bombieri, o que significa que o modelo estava a prolongar uma linha de investigação humana já existente, e não a inventar o campo do zero.

Porque é que a prova em Lean é o pormenor que importa

Um modelo de linguagem alargada a afirmar um novo limite matemático não é, por si só, prova de nada: os modelos produzem, com regularidade, provas fluentes mas erradas. O que muda o cálculo aqui é que a Claude não se limitou a enunciar o resultado, produziu uma formalização em Lean, um assistente de prova que verifica cada passo lógico face a um conjunto fixo de axiomas e regras de inferência, sem espaço para atalhos. A Anthropic relata que a formalização em Lean passa na validação automática padrão, o que constitui um tipo de prova categoricamente diferente de um modelo a afirmar que um número é verdadeiro.

Para além da verificação automática, a Anthropic fez o artigo ser revisto por especialistas externos: os teóricos dos números Brian Conrey e Dan Goldston examinaram o trabalho em cima da hora, juntamente com os próprios matemáticos da Anthropic, Levent Alpoge e Ralph Furman. Essa combinação, um verificador formal de provas mais especialistas humanos identificados, dispostos a associar o seu nome a uma revisão, é o que distingue este caso do fluxo constante de alegações matemáticas de IA não verificadas que circulam sem que ninguém as confirme.

Como isto se compara com 37 anos de progresso humano

A base histórica é o que torna este salto compreensível. O progresso sobre este limite específico tem sido lento, um esforço moroso ao longo de décadas: G.H. Hardy mostrou pela primeira vez, em 1914, que existem infinitos zeros sobre a linha crítica; Atle Selberg provou que uma proporção positiva dos zeros ali se situa; Norman Levinson chegou a cerca de um terço em 1974; o próprio Brian Conrey chegou a cerca de dois quintos em 1989; e a equipa Pratt-Robles-Zaharescu-Zeindler chegou aos 41,6 por cento em 2020. No conjunto, os matemáticos humanos moveram essa fração comprovável em cerca de 0,8 pontos percentuais ao longo dos 37 anos anteriores a esta execução.

O enxame da Claude moveu-a em 25,6 pontos percentuais em cerca de um dia e meio. Isto não significa que as máquinas sejam agora melhores matemáticos do que as pessoas que passaram esses 37 anos a construir as ferramentas em que a Claude se apoiou; a execução assentou explicitamente em resultados humanos já publicados por Baluyot, Goldston, Suriajaya, Turnage-Butterbaugh e Bombieri. É antes uma afirmação sobre a velocidade a que uma pesquisa bem dotada de recursos e bem verificada consegue avançar, uma vez existente o trabalho de base e havendo um grande enxame de agentes capaz de o explorar de forma exaustiva.

O que isto revela sobre a trajetória de capacidades dos laboratórios de fronteira

O modelo utilizado era explicitamente não lançado e de uso exclusivo para investigação, o que é, por si só, revelador. Significa que o fosso de capacidade entre aquilo que um laboratório de fronteira consegue demonstrar internamente e aquilo que chega aos clientes pagantes é suficientemente largo para produzir um resultado como este antes de o modelo subjacente ser tornado público. A Anthropic, a OpenAI e a Google DeepMind publicaram, cada uma, resultados adjacentes à matemática desta forma ao longo dos últimos dois anos, e o padrão é consistente: as versões internas de investigação são usadas para sondar os limites de capacidade em problemas difíceis e verificáveis, bem antes de qualquer lançamento comercial.

A arquitetura importa tanto quanto o modelo. Isto não foi uma conversa longa a produzir uma resposta longa; foi orquestração, dezenas de subagentes a trabalhar em paralelo, a maioria deles a falhar, com o processo principal a gerir a exploração e uma camada de validadores a verificar o trabalho candidato. Esse padrão de enxame mais verificador, e não a dimensão bruta do modelo, parece ser a parte que os laboratórios de fronteira estão atualmente a escalar mais depressa, e é também a parte com maior probabilidade de surgir em ferramentas comerciais de agentes muito antes de qualquer laboratório reivindicar a resolução de um problema em aberto na matemática pura.

O que os líderes de I&D europeus devem realmente reter

O teorema em si não vai alterar um balanço. O que é transferível para uma empresa europeia intensiva em I&D, um grupo farmacêutico a correr rastreios de moléculas, um fornecedor automóvel a iterar sobre materiais, um fabricante de chips a validar desenhos de circuitos, é o fluxo de trabalho: um grande enxame de agentes a atacar um problema em paralelo, a maioria dos quais se espera que falhe, filtrado por um verificador formal ou automático capaz de rejeitar respostas erradas sem necessitar de uma pessoa a validar cada candidato. Foi essa combinação que permitiu a um dia e meio de computação ultrapassar 37 anos de trabalho humano cuidadoso e credenciado sobre esta única questão restrita.

A ressalva honesta é que a matemática tem algo que a maioria dos problemas de I&D empresarial não tem: o Lean, um verificador capaz de provar a correção sem qualquer ambiguidade. A ciência dos materiais, as interações medicamentosas e a validação de circuitos têm equivalentes parciais, suites de simulação, testes físicos, ferramentas de verificação formal para a lógica de chips, mas raramente algo tão hermético como uma prova em Lean. A conclusão realista para um líder de I&D europeu que esteja a avaliar fluxos de trabalho assistidos por IA não é esperar, em breve, um momento equivalente à hipótese de Riemann no seu próprio domínio; é perguntar quais das ferramentas de verificação já existentes na sua organização, ainda que parciais, poderiam ser transformadas no filtro automático que torna um grande enxame de agentes digno de confiança, e não apenas rápido.