Google resolve nove problemas matemáticos que estavam décadas sem solução; OpenAI também

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.

Leia também: Tudo que sabemos sobre o maior IPO da história; SpaceX, uma empresa de I.A. com máscara de fogueteira

Como o sistema funciona

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.

Allan Ravagnani

Siga o Times Brasil - Licenciado Exclusivo CNBC no