LLMs provam teoremas, mas não descobrem matemática: pesquisadores descrevem o próximo passo

Um grupo de pesquisadores publicou um artigo de posicionamento no arXiv no início de julho de 2026 que sistematizou as conquistas de provadores de teoremas baseados em LLM e identificou sua limitação fundamental: os sistemas atuais provam teoremas mas são incapazes de descobrir matemática — e propôs um roteiro estratégico para a transição para agentes de pesquisa totalmente desenvolvidos.

O que os Sistemas AI4Math Conseguem Fazer Hoje

Nos últimos anos, os sistemas LLM para matemática formal alcançaram progresso tangível. Trabalhando com linguagens para prova interativa de teoremas (ITP) — principalmente Lean 4, Isabelle e Coq — aprenderam a gerar provas formais para problemas bem definidos. Essas linguagens permitem que as provas sejam escritas de forma que um computador possa verificar mecanicamente cada passo — tornando o resultado fundamentalmente mais confiável do que as provas tradicionais escritas à mão.

Os autores sistematizaram três direções principais de desenvolvimento da área:

• Datasets — corpora de problemas formalizados foram acumulados, variando do nível do ensino médio até o universitário, permitindo que modelos sejam treinados em exemplos de provas corretas
• Autoformalização — modelos melhoraram na tradução de enunciados de problemas escritos em linguagem natural para a sintaxe formal rigorosa do ITP
• Síntese de provas — os sistemas estão cada vez mais confiantes em encontrar provas passo a passo quando dada uma formulação inicial clara

Todas essas conquistas compartilham uma característica: funcionam apenas em problemas bem definidos e pré-formulados. O modelo sabe exatamente o que deve ser provado — e busca o caminho para esse objetivo.

Por Que Isto Ainda Não É Ciência

A verdadeira ciência matemática é fundamentalmente diferente de resolver listas de exercícios. Ela requer a capacidade de formular hipóteses, identificar conexões inesperadas entre diferentes domínios e atacar problemas abertos — frequentemente de longa data, mal formulados e exigindo múltiplos níveis de abstração. É exatamente aqui que os sistemas LLM atuais demonstram limitações sistêmicas.

Os autores identificam cinco problemas principais:

• Dados: os datasets não contêm exemplos de como novos teoremas nascem — apenas soluções de problemas já colocados
• Estrutura: a matemática se baseia em hierarquias complexas de conceitos e dependências implícitas entre ramos, que os LLMs assimilam mal
• Exploração: modelos conseguem responder perguntas mas não formular novas — e isso está no fundamento da ciência
• Ferramentas: não há integração com sistemas de álgebra computacional e bancos de dados matemáticos especializados
• Colaboração: modelos não conseguem ser colaboradores completos — não entendem o contexto informal que os cientistas transmitem uns aos outros

"O próximo avanço em AI4Math requer uma mudança decisiva de

solucionadores de tarefas predeterminadas para agentes de pesquisa capazes de trabalhar na fronteira da matemática" — a tese central do artigo.

Como Deveria Ser o Próximo Sistema

O roteiro estratégico descrito no artigo prevê uma transição para agentes de pesquisa matemática — sistemas capazes de formular independentemente hipóteses, planejar programas de pesquisa, interagir com cientistas em modo de diálogo e refinar iterativamente as formulações de problemas.

Isso exigirá o desenvolvimento simultâneo de várias direções: novos datasets com exemplos de descobertas reais, métodos para trabalhar com estruturas relacionais da matemática, ecossistemas de ferramentas mais maduros e modelos fundamentalmente diferentes de colaboração humano-máquina. Nenhum desses componentes existe ainda na forma necessária — tornando a tarefa em larga escala mas claramente formulada.

O que Isso Significa

O artigo sinaliza uma mudança importante no horizonte de AI4Math: de sistemas para verificação de provas para sistemas capazes de participar da descoberta de nova matemática. Essa transição requer arquitetura fundamentalmente diferente da simples ampliação das abordagens existentes. Se o roteiro proposto for implementado, a matemática pode se tornar um dos primeiros campos onde a IA se torna um verdadeiro parceiro de pesquisa do cientista.