AlphaProof Nexus do Google DeepMind resolve nove problemas abertos de Erdős, incluindo dois sem solução há 56 anos.
Sistema de IA do Google combina modelo de linguagem com verificador formal Lean para gerar provas matemáticas certificadas.
Google supera OpenAI em disputa por avanços em matemática com IA após anúncio rival na semana anterior.
Foto: Creative Commons Attribution
Google fecha acordo de US$ 920 milhões mensais com a SpaceX; veja
O Google DeepMind apresentou um avanço em matemática que coloca a inteligência artificial em território historicamente reservado a pesquisadores humanos. O sistema AlphaProof Nexus resolveu nove dos 353 problemas abertos de Erdős registrados na literatura matemática, incluindo dois que aguardavam solução há 56 anos.
🔍 Os problemas de Erdős são desafios matemáticos propostos pelo matemático húngaro Paul Erdős ao longo do século 20, muitos deles acompanhados de recompensas em dinheiro. Eles abrangem áreas como combinatória e teoria dos grafos e são considerados referências de dificuldade na matemática pura.
O resultado foi publicado em artigo científico submetido ao repositório arXiv em 21 de maio e chega um dia depois de a OpenAI ter anunciado que sua IA refutou uma conjectura de Erdős com 80 anos de existência.
O AlphaProof Nexus combina um modelo de linguagem de grande escala com o Lean, um assistente de verificação formal de provas matemáticas. O sistema gera uma prova, submete ao verificador e repete o processo até que uma versão seja aceita como matematicamente válida.
🔍 Lean é uma linguagem de programação usada para escrever e verificar provas matemáticas de forma automática. Diferente de uma calculadora, o Lean não apenas computa resultados — ele verifica se cada passo lógico de uma demonstração está rigorosamente correto.
Cada problema custou algumas centenas de dólares para ser resolvido. Além dos nove problemas de Erdős, o sistema também provou 44 conjecturas abertas da Enciclopédia Online de Sequências de Inteiros.
Disputa com a OpenAI
Na semana anterior, a OpenAI havia anunciado que seu modelo refutou de forma autônoma uma conjectura de Erdős com 80 anos, descrito pelo próprio Sam Altman como “um marco importante”. O Google respondeu com um resultado de escala maior – nove problemas contra um – e com verificação formal, o que garante que as provas são matematicamente certificadas, não apenas plausíveis.
O artigo científico foi submetido em 21 de maio e o sistema já está sendo implantado em pesquisas de combinatória, otimização, teoria dos grafos, geometria algébrica e óptica quântica.
Siga o Times Brasil no Google e receba as principais notícias do Brasil e do Mundo.
SoftBank despenca mais de 8% enquanto ações de tecnologia da Ásia caem, acompanhando perdas de Wall Street 
