Blog
Contato
5 Ideias Surpreendentes que Revelam Como a IA Está Aprendendo a Pensar como um Matemático
E se a Inteligência Artificial pudesse não apenas aprender com o conhecimento humano, mas também descobrir matemática do zero, apenas a partir de seus axiomas fundamentais.

by Carlos Costa

03 out. de 2025
A Nova Fronteira da Inteligência Artificial
Quando pensamos em inteligência artificial (IA) e matemática, a imagem que geralmente vem à mente é a de uma calculadora poderosa, capaz de resolver equações complexas em um piscar de olhos. E, de fato, os grandes modelos de linguagem (LLMs) modernos são excelentes em resolver problemas que terminam com uma resposta numérica. Mas o verdadeiro coração da matemática não está no cálculo, e sim no raciocínio — na construção de provas formais que demonstram a verdade de uma afirmação de maneira irrefutável.
Essa é uma fronteira muito mais desafiadora para a IA. Como destacam Yang et al. (2023, p. 1),
“Modelos de linguagem de larga escala (LLMs) têm mostrado potencial na demonstração de teoremas formais usando assistentes de prova como o Lean. Entretanto, os métodos existentes são difíceis de reproduzir ou de expandir, devido a código e dados privados, bem como a grandes exigências de computação” (tradução do autor).
Provar um teorema não é apenas encontrar um número; é construir uma cadeia lógica de argumentos, muitas vezes exigindo estratégia, intuição e criatividade. No entanto, pesquisas recentes estão revelando uma mudança fascinante. A IA não está apenas melhorando na resolução de problemas matemáticos; ela está começando a aprender a "pensar" como um matemático.
Este artigo explora cinco descobertas surpreendentes de pesquisas de ponta que mostram como a IA está desenvolvendo estratégias, curiosidade e até mesmo a capacidade de aprender com seus próprios erros, inaugurando uma era onde o próprio processo de descoberta pode ser automatizado.
A IA não está apenas aprendendo com humanos, mas descobrindo a matemática do zero.
A abordagem tradicional para ensinar matemática à IA consiste em alimentá-la com todo o conhecimento já produzido pela humanidade: livros didáticos, fóruns online, artigos acadêmicos e bibliotecas de provas formais escritas por especialistas. A ideia é que, ao absorver esse vasto oceano de dados, a IA aprenda a imitar os padrões do raciocínio humano.
No entanto, um projeto de pesquisa radical chamado MINIMO está virando essa lógica de cabeça para baixo. Em vez de depender do conhecimento humano, ele trata a matemática como um jogo que pode ser aprendido do zero, apenas com as "regras" — isto é, os axiomas fundamentais de um domínio matemático. Essa abordagem é inspirada no AlphaZero, a IA que dominou jogos como xadrez e Go sem estudar nenhuma partida humana, apenas jogando contra si mesma. Como explicam Poesia et al. (2024),
“Como a humanidade extraiu a matemática do éter? Exploramos a visão platônica de que a matemática pode ser descoberta a partir de seus axiomas — um jogo de conjectura e prova” (POESIA et al., 2024, p. 1, tradução do autor).
É uma ideia profundamente contraintuitiva: uma IA que constrói conhecimento matemático sem depender de milênios de descobertas humanas, explorando o universo da matemática por conta própria. Os pesquisadores argumentam que
“uma visão alternativa de como a IA pode dominar o raciocínio matemático enxerga a matemática pela lente dos jogos, observando que as regras do ‘jogo da matemática’ podem ser codificadas [...] a partir de um pequeno conjunto de axiomas” (POESIA et al., 2024, p. 2, tradução do autor).
A arte de perguntar — A IA está aprendendo a formular seus próprios problemas.
Em um jogo como o xadrez, o objetivo é claro: dar xeque-mate. Mas na matemática, o jogo é infinito. Um dos maiores desafios para o matemático não é apenas resolver problemas, mas também decidir quais valem a pena ser enfrentados. Essa habilidade de formular boas perguntas — ou “conjecturas” — é o que impulsiona a descoberta.
O projeto MINIMO aborda isso com um conceito chamado motivação intrínseca (intrinsic motivation). Como descrevem os autores:
““Descrevemos MINIMO (Mathematics via Intrinsic Motivation): um agente que aprende, de forma conjunta, a propor problemas desafiadores para si mesmo (conjecturar) e a resolvê-los (provar teoremas).” (Poesia et al., 2024, p. 1, tradução do autor).
O agente de IA não recebe uma lista de teoremas para provar. Em vez disso, ele aprende duas habilidades simultaneamente: conjecturar (propor novos problemas) e provar (resolver esses problemas).
Isso é crucial porque a IA desenvolve uma forma de “curiosidade”. Ela aprende a gerar problemas que estão no limite de sua capacidade atual — suficientemente desafiadores para promover o aprendizado, mas não tão difíceis a ponto de se tornarem impossíveis.Os pesquisadores explicam que:
“Nosso agente visa gerar conjecturas difíceis mas prováveis — um alvo em movimento, já que sua própria capacidade de prova de teoremas também melhora conforme treina” (POESIA et al., 2024, p. 1, tradução do autor).
Isso cria um ciclo virtuoso de autoaperfeiçoamento: ao resolver um problema que ela mesma formulou, a IA se torna mais inteligente e, em seguida, usa essa nova habilidade para propor problemas ainda mais complexos. Ela está, efetivamente, criando seu próprio currículo de aprendizado.
Esboçar primeiro, provar depois — A IA está imitando a estratégia humana para resolver problemas complexos.
Muitos métodos de IA para provar teoremas são considerados “míopes”. Eles tentam avançar passo a passo, otimizando a próxima ação com base no estado atual, mas frequentemente se perdem em detalhes que não levam a lugar algum. É como tentar escrever um livro complexo, palavra por palavra, sem nunca planejar a estrutura dos capítulos.
Criar Esboço
A IA primeiro cria um esboço da prova com os principais argumentos
Validar Lógica
O sistema verifica se a lógica geral do esboço está correta
Preencher Detalhes
A IA resolve recursivamente cada parte, uma por uma
Uma nova abordagem, chamada POETRY, resolve esse problema ensinando a IA a pensar de forma hierárquica, imitando uma estratégia típica de matemáticos para lidar com a complexidade. Essa abordagem foi implementada no assistente de provas Isabelle. Segundo Wang et al. (2024, p. 1):
“Tais abordagens são usualmente baseadas em heurísticas míopes (por exemplo, probabilidades log ou funções de valor) que frequentemente levam a subobjetivos subótimos ou até mesmo distratores, impedindo a descoberta de provas mais longas.” (tradução do autor).
Em vez de gerar uma prova longa e detalhada de uma só vez, a IA começa criando um esboço da prova (proof sketch). Os autores descrevem:
“Diferentemente de métodos passo-a-passo anteriores, POETRY busca por um esboço verificável da prova em cada nível e foca em resolver o teorema ou conjectura do nível atual. Provas detalhadas de conjecturas intermediárias dentro do esboço são temporariamente substituídas por uma tática de marcação chamada sorry, adiando suas provas para níveis subsequentes” (WANG et al., 2024, p. 1, tradução do autor).
Funciona como escrever um ensaio: primeiro, você cria um esboço com os principais argumentos e, em seguida, preenche os detalhes de cada seção. No POETRY, a IA delineia os passos principais da prova e usa um comando especial chamado "sorry" como um marcador de posição para os detalhes das subprovas. Isso permite que o sistema verifique se a lógica geral do esboço está correta antes de mergulhar nos detalhes. Uma vez que o esboço é validado, a IA volta e resolve recursivamente cada "sorry", um por um.
Essa abordagem de "esboçar primeiro, provar depois" se mostrou incrivelmente eficaz. Como reportam os pesquisadores:
“observamos um aumento substancial no comprimento máximo das provas encontradas pelo POETRY, de 10 para 26” (WANG et al., 2024, p. 1, tradução do autor).
Isso permitiu que a IA encontrasse provas muito mais longas e complexas. Mas uma boa estratégia não é nada sem a capacidade de se recuperar de becos sem saída. Surpreendentemente, a IA também está aprendendo essa resiliência.
O fracasso é um professor — Como a IA transforma erros em novas descobertas.
Na ciência e na matemática, o fracasso raramente é um beco sem saída. Uma experiência malsucedida ou uma tentativa de prova que não deu certo pode, muitas vezes, revelar uma verdade inesperada. Surpreendentemente, a IA também está aprendendo essa lição.
No projeto MINIMO, os pesquisadores implementaram uma técnica genial chamada re-rotulagem retrospectiva (hindsight relabeling). Poesia et al. (2024) explicam:
“Propomos novos métodos de re-rotulagem retrospectiva em árvores de busca de provas para melhorar significativamente a eficiência amostral do agente em ambas as tarefas.” (Poesia et al., 2024, p. 1, tradução do autor).
Imagine que a IA se propõe a provar a "Conjectura A". Ela tenta vários caminhos, aplica axiomas, mas no final, falha. Em vez de simplesmente descartar essa tentativa como um erro, o sistema analisa a trajetória da falha.
Objetivo Original
Tentar provar que
2+1=0
Descoberta Acidental
Através de manipulações válidas, chegar à prova de que:
2+1=3
Nova Verdade
Reconhecer que uma verdade inesperada foi revelada
Ele pode descobrir que, embora não tenha provado a Conjectura A, a cadeia de passos lógicos que seguiu acidentalmente provou uma "Conjectura B" completamente nova e desconhecida. Por exemplo, ao tentar provar que 2 + 1 = 0, a IA pode, através de manipulações válidas, chegar à prova de que 2 + 1 = 3. A genialidade está em reconhecer que, mesmo partindo de uma conjectura falsa, a aplicação de regras lógicas válidas pode, por si só, revelar uma verdade inesperada no caminho.
Essa técnica aumenta drasticamente a eficiência do aprendizado. Cada falha se converte em fonte de novos dados de treinamento e em potenciais descobertas matemáticas. Em vez de aprender apenas com o sucesso, a IA extrai conhecimento valioso de seus próprios erros — característica fundamental do aprendizado autêntico e da descoberta científica.
Uma "biblioteca" inteligente vale mais que memorização pura.
Provar um teorema raramente é um ato isolado. Quase sempre, depende do uso de teoremas, lemas e definições previamente estabelecidos, armazenados em vastas bibliotecas matemáticas. Um dos maiores desafios para a IA é escolher, entre centenas de milhares de “ferramentas” disponíveis, quais utilizar em um determinado passo da prova.
Métodos anteriores dependiam da simples memorização do LLM. O modelo precisava “lembrar” de ter visto uma premissa semelhante em um contexto parecido durante o treinamento. Essa abordagem pode funcionar, mas não generaliza bem para cenários realmente novos.
O projeto LeanDojo introduziu o modelo ReProver (Retrieval-Augmented Prover), que adota uma estratégia muito mais eficiente. Yang et al. (2023) descrevem:
“Ele contém anotações detalhadas de premissas em provas, fornecendo dados valiosos para a seleção de premissas — um gargalo-chave na demonstração de teoremas. Usando esses dados, desenvolvemos o ReProver (Retrieval-Augmented Prover): um provador baseado em LLM, aprimorado com recuperação para selecionar premissas de uma vasta biblioteca matemática.” (Yang et al., 2023, p. 1, tradução do autor).
Em vez de tentar memorizar toda a biblioteca, ele aprende a pesquisar e recuperar a informação certa quando precisa.

É como a diferença entre um estudante que tenta decorar todos os livros de uma biblioteca e um pesquisador experiente que sabe usar o catálogo para encontrar exatamente o que precisa.
Os pesquisadores frisam que
“Nosso recuperador aproveita a capacidade de análise de programas do LeanDojo para identificar premissas acessíveis e exemplos negativos difíceis, o que torna a recuperação muito mais eficaz” (YANG et al., 2023, p. 1, tradução do autor).
O ReProver aprende a olhar para o estado atual da prova e a consultar eficientemente a biblioteca para encontrar as premissas mais relevantes. Essa abordagem mostrou-se muito mais eficaz, superando inclusive o GPT-4 nos testes reportados pelos autores.
De Calculadoras a Colaboradores Criativos
As cinco ideias exploradas apontam para uma transformação fundamental. Ao aprender do zero, formular suas próprias perguntas, esboçar estratégias, aprender com os erros e consultar bibliotecas de conhecimento, a IA passa a espelhar o próprio processo de descoberta matemática. Ela está evoluindo de uma ferramenta que apenas executa tarefas para um parceiro capaz de estratégia, curiosidade e descoberta.
Descoberta Autônoma
Aprendendo matemática do zero, sem depender do conhecimento humano.
Curiosidade Artificial
Formulando suas próprias perguntas e criando currículos de aprendizado.
Estratégia Hierárquica
Esboçando primeiro e preenchendo detalhes depois.
Aprendizado com Erros
Transformando falhas em novas descobertas matemáticas.
Pesquisa Inteligente
Consultando bibliotecas de conhecimento de forma eficiente.
Como demonstram os avanços em MINIMO, POETRY e ReProver, não estamos mais diante apenas da automação de cálculos, mas da automação do próprio processo de raciocínio. A IA está desenvolvendo habilidades que, por muito tempo, consideramos exclusivamente humanas.
Isso nos leva a uma pergunta provocativa:
Se a IA pode descobrir novas matemáticas sem recorrer à intuição humana, que territórios desconhecidos do conhecimento ela nos ajudará a explorar e até que ponto podemos considerar esse conhecimento como ciência autêntica — e não apenas como uma engenhosa simulação?
Fontes
Este artigo de divulgação científica se apoia em pesquisas recentes que investigam como a inteligência artificial está transformando a prática matemática, em especial no campo das provas formais. Os principais trabalhos consultados foram:
  • POESIA, G. et al. Learning Formal Mathematics From Intrinsic Motivation. arXiv:2407.00695 [cs.LG]. DOI: 10.48550/arXiv.2407.00695.
  • YANG, K. et al. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. arXiv:2306.15626 [cs.LG]. DOI: 10.48550/arXiv.2306.15626.
  • YANG, K. et al. Lean Workbook: A Large-Scale Lean Problem Set Formalized From Natural Language Math Problems. arXiv:2406.03847 [cs.CL]. DOI: 10.48550/arXiv.2406.03847.