Publicado em 8 de outubro de 2026, um artigo na Science relata que o AlphaProof Nexus, sistema de pesquisa de provas matemáticas formais da Google DeepMind, resolveu 9 dos 353 problemas abertos de Erdős avaliados. O mesmo trabalho registra 44 conjecturas provadas entre 492 conjecturas abertas da Online Encyclopedia of Integer Sequences (OEIS).
O que o artigo relata
Duas das questões de Erdős resolvidas estavam em aberto havia 56 anos. Em outra coleção avaliada, a OEIS, o sistema provou 44 das 492 conjecturas abertas consideradas no estudo.
Os resultados dizem respeito a dois conjuntos distintos: problemas abertos de Erdős e conjecturas da OEIS. Cada proporção descreve seu respectivo conjunto avaliado, não o desempenho geral da IA em matemática.
Como geração de provas e Lean trabalham juntos
O AlphaProof Nexus alterna a geração de provas por um modelo de linguagem (LLM) com a verificação formal no Lean, um assistente de provas cujo compilador checa os passos formais. O sistema propõe uma prova; o Lean verifica se os passos atendem às regras formais.
O artigo também relata que um agente básico, alternando geração por LLM e verificação pelo Lean, reproduziu os nove resultados obtidos nos problemas de Erdős.
