Um estudo do Google DeepMind publicado em 8 de outubro de 2026 relata que o AlphaProof Nexus provou 9 de 353 problemas de Erdős formalizados e 44 de 492 conjecturas selecionadas da Online Encyclopedia of Integer Sequences (OEIS). Dois dos problemas de Erdős resolvidos estavam em aberto havia 56 anos. O sistema combina agentes de inteligência artificial com o Lean, um assistente que verifica provas matemáticas formalizadas.
O que o AlphaProof Nexus faz
O AlphaProof Nexus é uma estrutura de busca por provas formais: recebe um enunciado matemático expresso em Lean e um esboço de prova, e usa modelos de linguagem para propor ou revisar trechos dessa prova. O Lean compila e verifica as tentativas, fornecendo retorno que orienta novas alterações.
Uma prova formal é escrita em uma linguagem precisa o bastante para que um sistema possa conferir cada passo. Isso permite verificar mecanicamente se uma demonstração decorre do enunciado codificado, em vez de depender apenas de uma explicação plausível em linguagem natural.
O que os resultados medem
O estudo avaliou dois conjuntos diferentes. Os resultados relatados foram:
| Conjunto avaliado | Problemas ou conjecturas provados | Itens avaliados | Escopo |
| Problemas de Erdős | 9 | 353 | Problemas formalizados em Lean e avaliados no estudo |
| Conjecturas da OEIS | 44 | 492 | Conjecturas abertas selecionadas para a avaliação |
Os 353 casos de Erdős correspondiam aos problemas formalizados em Lean no conjunto usado na avaliação. Dois dos nove resolvidos estavam em aberto havia 56 anos. Já os 44 resultados da OEIS pertenciam a outro conjunto: o estudo relata que uma revisão manual considerou as conjecturas corretamente formalizadas e ainda sem prova anterior.
As duas contagens têm populações próprias. Juntá-las em uma única taxa esconderia que os conjuntos foram selecionados e avaliados separadamente.
Como funciona a busca por provas
O processo começa com um teorema e um esboço de prova em Lean. O sistema pode receber também contexto em linguagem natural e conhecimento do domínio codificado em Lean. Os agentes de linguagem fazem alterações nas tentativas; a compilação no Lean indica se a prova formal passa pela checagem e ajuda a orientar as próximas revisões.
Na configuração mais completa, o framework reúne e seleciona esboços de prova por busca evolutiva e pode chamar o AlphaProof, um sistema especializado, para trabalhar em subproblemas. Essa combinação amplia as estratégias de busca dentro da prova formalizada, mas o ponto de partida descrito no estudo continua sendo um enunciado em Lean acompanhado de um esboço.
O que os resultados mostram
A checagem do Lean responde a uma pergunta específica: a prova apresentada demonstra o enunciado formal que foi codificado? Ela não determina, por si só, se essa formalização representa fielmente a intenção da pergunta matemática original. Para os enunciados de Erdős, o estudo relata uma revisão especializada das formalizações.
A maioria dos problemas de Erdős avaliados permaneceu sem solução. Os autores também situam os êxitos sobretudo em áreas como combinatória, otimização convexa e teoria dos números, onde as bibliotecas matemáticas do Lean são mais maduras e os problemas podem ser divididos em subetapas tratáveis.
