AlphaProof Nexus, do Google DeepMind, resolve 9 problemas em aberto de Erdős

O sistema AlphaProof Nexus, do Google DeepMind, resolveu de forma autônoma 9 dos 353 problemas em aberto de Paul Erdős que tentou, dois deles sem resposta há 56 anos, a um custo de algumas centenas de dólares por solução. Ele também provou 44 de 492 conjecturas da Enciclopédia On-line de Sequências Inteiras e melhorou um resultado em otimização convexa.

O sistema usa o modelo de linguagem Gemini 3.1 Pro para gerar passos de demonstração em Lean, uma linguagem formal cujo compilador verifica cada etapa, deixando aos humanos apenas a conferência final. O anúncio reforça uma disputa com a OpenAI, que dias antes usou um modelo próprio para derrubar a conjectura das distâncias unitárias de Erdős.