O que o artigo afirma
Uma equipa da Google DeepMind publicou um relato revisto por pares de um sistema de IA que encontra demonstrações matemáticas e as submete a verificação automática à medida que avança. O artigo, “Advancing Mathematics Research with AI-Driven Formal Proof Search”, de Tsoukalas e colegas, saiu na Science a 8 de outubro.
O sistema, AlphaProof Nexus, está construído em torno do Gemini 3.1 Pro. Redige uma demonstração em Lean, uma linguagem formal em que cada passo lógico é verificado por software, e as mensagens de erro do verificador orientam o rascunho seguinte. Para subproblemas mais difíceis pode passar a tarefa ao AlphaProof, a ferramenta especializada da DeepMind.
Os investigadores escolheram 353 problemas abertos da coleção de Erdős e codificaram-nos em Lean. O sistema fechou nove deles — cerca de 2,5% — dois dos quais estavam por resolver há 56 anos. Demonstrou também 44 conjeturas da Enciclopédia Online de Sequências de Inteiros, resolveu uma questão aberta de geometria algébrica e melhorou um limite conhecido em otimização min-max, uma técnica usada no treino de alguns modelos de IA.
A ablação é a parte interessante
A DeepMind informa que o sistema resolveu os mesmos nove problemas de Erdős sem o AlphaProof. Uma análise de ablação verificou que uma configuração mais simples, a que o artigo chama Agente A, chegou aos mesmos nove, ponto levantado por Josep Curto, da Universidade Aberta da Catalunha, nos comentários de peritos reunidos pelo Science Media Centre España. Curto lê o resultado como sinal de sobre-engenharia e sustenta que o artigo arrasta incoerências metodológicas.
A sua objeção mais afiada é sobre o que a verificação formal compra e não compra. O Lean, nota, garante que uma demonstração é logicamente válida. Não garante que o enunciado que alguém formalizou seja o problema que pretendia enunciar. A tradução de uma conjetura informal para Lean continua a ser um passo humano, e um erro aí sobrevive intacto ao verificador.
Como se deve ler nove em 353
O denominador importa. São nove êxitos num conjunto definido que a equipa escolheu e formalizou, não uma capacidade geral de derrubar conjeturas célebres. Pablo Haya Coll, da Universidade Autónoma de Madrid, no mesmo conjunto de comentários, aponta a metodologia e não a contagem: o valor está numa forma repetível de gerar descobertas matemáticas, não nos nove.
Javier Aramayona, que dirige o Instituto de Ciências Matemáticas espanhol, levanta o problema que decorre de demonstrações verificadas chegarem mais depressa do que alguém as lê: muitos resultados gerados por IA estão verificados e, ainda assim, não são plenamente compreendidos. Teodoro Calonge, da Universidade de Valladolid, chamou-lhe um artigo de alta qualidade e uma tentativa inicial, com margem considerável para melhorar.
O contraste com o outro laboratório
O caminho que este trabalho seguiu é parte da história. A DeepMind publicou as soluções de Erdős antes de o artigo sair e depois submeteu o trabalho a revisão por pares. A OpenAI seguiu o outro caminho e colocou centenas de demonstrações geradas por IA num repositório, o que levou um grupo de matemáticos a pedir um boicote à empresa no início deste mês.
O que convém vigiar é se os ficheiros Lean resistem ao escrutínio externo, e se alguma das nove formalizações acaba por enunciar algo diferente do problema de Erdős a que está associada. Essa verificação está agora ao alcance de qualquer pessoa, que é o argumento prático a favor do caminho escolhido pela DeepMind.
