Imagine o mundo da matemática como uma biblioteca gigante e infinita. Por muito tempo, os alunos de IA mais inteligentes nesta biblioteca foram como brilhantes Solucionadores (Solvers). Eles eram incríveis em pegar uma tarefa de casa específica e bem escrita, ler as instruções e encontrar a resposta. Se você desse a eles um problema matemático de uma competição de ensino médio, eles poderiam frequentemente resolvê-lo mais rápido que um gênio humano. Eles eram como carros de corrida em uma pista perfeitamente pavimentada: rápidos, precisos e confiáveis.

Mas os autores deste artigo argumentam que estamos atingindo um muro. Esses Solucionadores são ótimos em terminar a corrida, mas não conseguem inventar a corrida. Eles não conseguem olhar para a biblioteca, encontrar um mistério empoeirado e não resolvido que está parado lá há décadas e descobrir uma maneira totalmente nova de decifrá-lo.

O artigo sugere que é hora de parar de construir melhores carros de corrida e começar a construir Agentes de Pesquisa (Research Agents). Estes não são apenas estudantes que seguem instruções; são exploradores que podem vagar pelo desconhecido, perder-se, tentar ideias estranhas e, talvez — apenas talvez — descobrir algo novo.

O Estado Atual: A Era do "Solucionador"

Atualmente, a IA está arrasando em desafios conhecidos.

• O Benchmark MiniF2F: Este é como um teste de matemática de ensino médio super difícil. Em 2021, a IA acertou cerca de 30%. Até julho de 2025, um sistema chamado Seed-Prover obteve 99,6% (243 de 244 problemas) de acerto. É basicamente uma pontuação perfeita.
• O IMO (Olimpíada Internacional de Matemática): Estes são os problemas mais difíceis para os melhores estudantes de ensino médio do mundo. Em 2024, uma IA chamada AlphaProof obteve um nível de pontuação de "Medalha de Prata". Até julho de 2025, o Seed-Prover resolveu 5 de 6 problemas da competição de 2025.

Isso é enorme! Prova que a IA pode fazer matemática rigorosa e verificada por máquinas. Mas aqui está o detalhe: todos esses são problemas onde a resposta já existe no universo da matemática. A IA está apenas encontrando o caminho para um tesouro conhecido.

O Problema: A "Lacuna de Pesquisa"

O artigo aponta que a pesquisa matemática real é bagunçada. Não é um teste de múltipla escolha. É como tentar encontrar uma agulha em um palheiro, mas você nem sabe ainda qual é a aparência da agulha.

Os autores argumentam que os sistemas de IA atuais são fundamentalmente limitados quando se trata de "pesquisa de fronteira".

• A Armadilha da "Redescoberta": Quando a IA afirma resolver um problema aberto famoso (como um da lista de Problemas de Erdős, uma coleção de mais de 1.100 enigmas matemáticos difíceis), ela muitas vezes apenas encontra uma solução que humanos já escreveram em um livro, mas que a IA não conhecia.
• O Risco de "Alucinação": Se você pedir a uma IA para resolver um problema cuja resposta ela não conhece, ela pode simplesmente inventar uma prova que parece correta, mas que é, na verdade, um absurdo. Ao contrário de um humano que pode dizer: "Estou travado, preciso de uma nova ideia", a IA muitas vezes camamente caminha com confiança em direção ao abismo.

O artigo explicitamente descarta a ideia de que a IA atual esteja pronta para ser um matemático solo descobrindo o próximo grande teorema. Eles dizem que sistemas como DeepSeek-Prover ou AlphaProof ainda são apenas "Solucionadores", não "Pesquisadores". Eles ainda não conseguem enfrentar os gigantes verdadeiramente não resolvidos, como a Hipótese de Riemann ou as equações de Navier-Stokes, sem ajuda humana.

O Roteiro: Do Solucionador ao Pesquisador

Então, como transformamos um carro de corrida em um explorador? Os autores traçam um mapa com cinco grandes obstáculos a serem superados:

1. O Deserto de Dados
Imagine tentar aprender a escrever um romance lendo apenas 10 páginas de texto. Esse é o problema da matemática formal. Enquanto existem bilhões de palavras de texto normal na internet, existem apenas cerca de 1,3 milhão de linhas de código matemático formal (em um sistema chamado Lean).

• A Solução: Precisamos ensinar a IA a traduzir a "matemática humana" (que é vaga e depende de contexto) para a "matemática computacional" (que é super precisa). Isso é chamado de Autoformalização. O artigo sugere que isso está melhorando, mas ainda é complicado. Um erro minúsculo na tradução pode fazer um problema difícil parecer fácil, ou um problema fácil parecer impossível.

2. O Mapa Ausente
A IA atual trata cada problema matemático como uma ilha separada. Mas, na matemática real, tudo está conectado. Uma prova em geometria pode depender de um lema da álgebra.

• A Solução: Precisamos construir um Grafo de Conhecimento gigante. Imagine uma teia onde cada teorema é um nó, e as linhas que os conectam mostram como eles se relacionam. Se a IA puder ver essas conexões, ela poderá usar ideias antigas para resolver novos problemas, em vez de começar do zero toda vez.

3. De Verificar para Descobrir
No momento, a IA é ótima em verificar se uma prova está correta (Verificação). Ela é ruim em criar a prova em si (Descoberta).

• A Solução: Precisamos de sistemas que possam conjecturar (supor) novos teoremas e então tentar prová-los. Alguns experimentos, como o AlphaEvolve, estão tentando fazer isso permitindo que a IA "evolua" novas ideias, de forma semelhante a como a natureza evolui as espécies. Mas o artigo observa que isso ainda está nos estágios iniciais; a IA ainda não consegue inventar um novo conceito matemático (como um novo tipo de número) da mesma forma que um gênio humano pode.

4. O Cinto de Ferramentas
Matemáticos humanos não usam apenas seus cérebros; eles usam calculadoras, computadores e softwares para fazer o trabalho pesado.

• A Solução: A IA precisa aprender a usar essas ferramentas também. Mas há um porém: se a IA pedir a uma calculadora para fazer uma soma, como ela saberá que a calculadora não cometeu um erro? O artigo sugere que precisamos de melhores formas para a IA verificar o trabalho dessas ferramentas externas para não ser enganada.

5. A Dança Humano-IA
O artigo argumenta que o futuro não é "IA vs. Humano". É IA + Humano.

• A Solução: Pense na IA como um assistente de pesquisa super veloz. Ela pode ler milhares de artigos em um segundo, verificar 1.000 provas possíveis e organizar os dados. O humano é o Capitão, fornecendo a intuição, o "pressentimento" e o julgamento final sobre se uma ideia é realmente brilhante ou apenas uma alucinação.
• Exemplo do mundo real: No final de 2025, um agente de IA chamado Aristotle ajudou a resolver um problema da lista de Erdős. Ele gerou uma prova, mas acabou resultando que o problema que ele resolveu era uma versão ligeiramente "enfraquecida" do original. Os matemáticos humanos tiveram que intervir para perceber que o problema original ainda estava em aberto. Isso mostra que, embora a IA seja poderosa, ela ainda precisa de um humano para mantê-la honesta.

A Conclusão

O artigo é um chamado à ação. Ele diz: "Construímos Solucionadores incríveis. Eles podem vencer qualquer competição de matemática. Mas para expandir os limites do conhecimento humano, precisamos construir Agentes de Pesquisa."

Esses agentes não apenas seguirão as regras; eles nos ajudarão a escrever novas regras. Mas o artigo é claro: não chegamos lá ainda. A IA é atualmente um aprendiz brilhante, não um mestre. Ela precisa de melhores dados, melhores mapas, melhores ferramentas e, o mais importante, um parceiro humano para guiá-la através dos territórios escuros e inexplorados da matemática.

A jornada do "Resolver" para o "Descobrir" é o próximo grande salto, e será necessário um esforço de equipe para chegar lá.