Modelo não lançado da Anthropic avança na hipótese de Riemann

A Anthropic anunciou na segunda-feira que um modelo ainda não lançado fez progresso significativo na hipótese de Riemann, um dos maiores problemas em aberto da matemática há mais de 150 anos. Segundo a empresa, o modelo aumentou de forma expressiva o limite inferior de soluções para as quais a hipótese se mantém verdadeira.

A hipótese de Riemann trata da distribuição dos números primos e permanece sem prova geral. Há atualmente uma recompensa de US$ 1 milhão para quem apresentar uma demonstração válida, valor ainda não reclamado. O modelo da Anthropic não resolveu o problema, mas foi mais longe do que se esperaria de uma IA atual, segundo o relato.

Como o resultado foi obtido

O ponto mais notável, de acordo com a fonte, é o método. Um funcionário da Anthropic sem formação matemática relevante pediu ao modelo para "dar uma tentativa real" ("take a real stab") de provar a hipótese e depois deixou o modelo coordenar a tarefa ao longo de um dia e meio.

Ao todo, o modelo testou 650 ideias diferentes para atacar o problema, coordenando 60 subagentes. A distribuição de papéis, descrita em nota de rodapé do paper, foi:

• 2 subagentes responsáveis por desenvolver as ideias matemáticas centrais;
• 13 que contribuíram com ideias para esses agentes;
• 30 que tentaram (sem sucesso) desenvolver novas ideias;
• 13 atuando como validadores para checar a correção dos argumentos;
• 2 que ajudaram a escrever o paper inicial.

O resultado foi confirmado por dois matemáticos internos da Anthropic e formalizado usando o assistente de prova de código aberto Lean.

Parte de uma sequência de resultados

O episódio se soma a uma série de avanços matemáticos liderados por LLMs neste ano. Vários problemas de Erdős foram resolvidos por modelos de IA ao longo de 2026. A OpenAI divulgou recentemente dez resultados provados por seu modelo interno "Astra", e um esforço separado da própria Anthropic refutou a conjectura de Jacobi (Jacobian conjecture).

O debate na comunidade matemática

O acúmulo de resultados gerou tanto entusiasmo quanto preocupação. Em uma declaração pública assinada em junho, um grupo de matemáticos de destaque levantou o receio de que a IA possa minar valores centrais da área, em especial o padrão de que provas verdadeiras devem ser "atribuíveis a autores específicos, que assumem crédito por sua descoberta e responsabilidade por sua correção".

O campo segue dividido. Em resposta à declaração, o vencedor da Medalha Fields Timothy Gowers questionou se a influência da IA não poderia mudar a matemática de forma mais complexa e positiva: "Se chegarmos a um mundo em que teoremas matemáticos não estão mais associados a matemáticos, talvez isso não seja mais problemático do que o fato de estrelas não levarem o nome de astrônomos e a maioria não ter nome nenhum", escreveu.

Por que isso importa para quem constrói software no Brasil

Para devs brasileiros que trabalham com modelos de linguagem, o caso é menos sobre matemática pura e mais sobre arquitetura de agentes. O que a Anthropic descreve é um sistema multiagente com divisão explícita de papéis (geração de ideias, tentativa, validação e redação), coordenado autonomamente por dias, e cujo resultado passou por verificação formal no Lean, não apenas por avaliação de linguagem natural.

Esse é um padrão replicável em produtos: separar agentes geradores de agentes validadores, e sempre que possível ancorar a saída em um verificador determinístico (compilador, testes, prova formal) em vez de confiar no próprio modelo para julgar a própria resposta. Também vale notar o custo e o tempo envolvidos: um dia e meio de execução coordenada não é um prompt barato, o que reforça que orquestração de agentes de longa duração exige planejamento de infraestrutura e orçamento.

Como o modelo ainda não foi lançado, não há acesso público às capacidades descritas. Vale acompanhar o Lean e os anúncios oficiais da Anthropic para quem quiser experimentar fluxos de verificação formal assistida por IA.

Fonte: TechCrunch