AlphaProof Nexus da DeepMind resolve problemas de Erdős e passa por revisão por pares

O sistema opera com o modelo Gemini 3.1 Pro no centro de sua arquitetura. O modelo rascunha e revisa argumentos formais escritos na linguagem Lean. O Lean funciona como verificador interativo: examina cada rascunho após qualquer edição e emite mensagens de erro que direcionam a tentativa seguinte do modelo. O ciclo de correção roda de forma contínua. Quando enfrenta subproblemas mais complexos, o sistema aciona o AlphaProof, uma ferramenta complementar especializada em provas matemáticas.

Lean valida os rascunhos e dispensa ferramenta extra em desafios históricos

A própria DeepMind informou que o sistema resolveu os nove problemas de Erdős sem precisar acionar o AlphaProof. Essa autonomia coloca o peso da dedução matemática nas iterações entre o Gemini 3.1 Pro e o checador Lean. Além dos nove problemas de Erdős, o AlphaProof Nexus provou 44 conjecturas da base de dados de sequências inteiras OEIS. O sistema também resolveu uma questão em aberto na área de geometria algébrica. Os pesquisadores haviam compartilhado as soluções dos problemas de Erdős na internet antes de publicar o artigo científico.

O modelo avançou também em problemas aplicados à própria computação. Ele melhorou um limite conhecido no campo da otimização min-max, técnica matemática usada no treinamento de modelos de inteligência artificial. O cálculo refina parâmetros teóricos de treino. Manuel Uth relatou no The Decoder que o trabalho se apoiou integralmente na verificação por compilador formal. Essa checagem impede que alucinações comuns a modelos de linguagem entrem na versão final do texto matemático.

Publicação na Science responde a boicote contra despejo de dados no GitHub

A divulgação do trabalho chega no momento em que matemáticos contestam métodos de concorrentes da DeepMind. A OpenAI enfrentou reação negativa recente após despejar centenas de provas geradas por inteligência artificial diretamente no GitHub, sem submetê-las a periódicos acadêmicos. O despejo sem crivo editorial gerou revolta entre especialistas que trabalham checando teoremas manualmente. A Association for Human Mathematics, liderada por Terence Tao, convocou um boicote contra a conduta da OpenAI. A iniciativa de Tao cobra responsabilidade científica das empresas de inteligência artificial.

A Google DeepMind optou por submeter o AlphaProof Nexus à revista Science antes de anunciar os resultados como consolidados. Essa validação externa diferencia o comunicado da DeepMind de relatórios técnicos internos que empresas do setor costumam postar em blogs corporativos. Mesmo com o aval dos revisores da Science, a empresa não detalhou no estudo o consumo de energia ou o tempo total de processamento exigido para cada prova ser concluída. A liberação pública de código ou de acesso direto ao sistema também não consta no anúncio oficial.