O sistema de demonstração matemática AlphaProof Nexus, do Google DeepMind, foi publicado oficialmente na Science. O primeiro autor do artigo é Tsoukalas, e toda a equipe de pesquisa pertence à DeepMind. O trabalho já havia sido divulgado como pré-print no fim de maio; agora chega a versão de periódico, depois da revisão por pares.
O placar continua o mesmo: o sistema tentou 353 problemas de Erdős ainda não resolvidos e solucionou 9, dois deles em aberto havia 56 anos; entre as 492 conjecturas abertas da OEIS, a base de dados de sequências de números inteiros, provou 44. Além disso, respondeu a uma pergunta de geometria algébrica sobre a função de Hilbert, pendente havia cerca de 15 anos, e melhorou um limite conhecido em otimização min-max.
Um Gemini e um compilador Lean
A base do sistema é o Gemini 3.1 Pro. O modelo redige demonstrações na linguagem formal Lean; o compilador Lean verifica a cada alteração, e as mensagens de erro voltam diretamente para a tentativa seguinte. Ao longo de todo o processo, o humano só olha o resultado no final.
O artigo separa quatro versões:
- Versão A: o ciclo “gerar e verificar” mais simples, em que o modelo grande escreve e o compilador julga;
- Versão B: sobre a A, incorpora o AlphaProof, o provador anterior da DeepMind, voltado a preencher os trechos que faltam na demonstração;
- Versão C: adiciona um mecanismo evolutivo, no qual vários subagentes compartilham um conjunto de rascunhos de demonstração ordenado por pontuação Elo;
- Versão D: tudo isso somado, usado para atacar os problemas de Erdős.
O dado mais curioso do resultado é que a versão A também provou, de forma independente, os 9 problemas de Erdős; só que, nos mais difíceis, gastou mais dinheiro. O custo de inferência citado pelo The Decoder é de algumas centenas de dólares por problema. Os autores escrevem no artigo:
"power of compiler feedback in grounding LLM reasoning"
(O feedback do compilador ancora o raciocínio dos grandes modelos de linguagem na realidade.)
As ressalvas de acadêmicos espanhóis
No dia em que o artigo foi publicado, o Science Media Centre da Espanha consultou vários pesquisadores do país, e as opiniões se dividiram.
Pablo Haya Coll, pesquisador da UAM, considera que o método consegue produzir de forma sistemática descobertas matemáticas de peso. Josep Curto, da UOC, avaliou que se trata de "a dazzling display of technical capability marred by significant methodological inconsistencies", ou seja, uma exibição tecnicamente deslumbrante, mas com inconsistências metodológicas evidentes. Ele apontou três pontos: o fato de A e D resolverem os mesmos problemas indica que a complexidade do arcabouço não determina necessariamente a capacidade de descoberta; o custo considera apenas as execuções bem-sucedidas, e a conta de B e D tampouco inclui o gasto de inferência do próprio AlphaProof; o Lean só garante que a demonstração vale para “a proposição que foi escrita”, e se essa proposição traduz fielmente o problema original ainda depende da conferência manual de matemáticos, e o artigo admite que houve erros de formalização.
O diretor do ICMAT, Javier Aramayona, preocupa-se com outra coisa: o surgimento de uma enxurrada de resultados “sabidamente verdadeiros, mas que ninguém compreende por completo”, o que pode enfraquecer a etapa da compreensão na pesquisa matemática e a formação de jovens pesquisadores. Teodoro Calonge, da Universidade de Valladolid, foi mais direto: a área ainda tem bastante margem para melhorar.
Os próprios autores deixam claro o alcance: a taxa geral de sucesso da IA em problemas de Erdős fica em torno de 1% a 2%, os resolvidos são em sua maioria relativamente fáceis e se concentram em combinatória, otimização convexa e teoria dos números, áreas em que a biblioteca Mathlib é mais densa e os problemas se decompõem bem em submetas. Problemas que exigem inventar muita teoria nova ficam praticamente fora do alcance do sistema.
Juntando os fatos deste ano
Em maio, noticiamos que um modelo da OpenAI resolveu uma conjectura de Erdős de 80 anos; em setembro, houve uma disputa de autoria entre matemáticos e a OpenAI; em 6 de outubro, a OpenAI liberou de uma só vez no GitHub 722 manuscritos matemáticos gerados por IA, em um repositório de código aberto com licença Apache 2.0, sem passar por periódico. O The Decoder informa que um grupo de matemáticos liderado por Terence Tao pediu em seguida o boicote a essa prática.
A diferença entre as duas empresas fica nítida. A OpenAI escolheu volume e abertura, deixando a triagem para a comunidade; a DeepMind escolheu um número muito menor de resultados, mas cada um passou pelo compilador Lean e também pela revisão de um periódico. Quanto ao papel do Lean, a DeepMind é bem comedida no artigo; a frase original é que a verificação formal "can serve as a filter for determining which proofs merit human review", isto é, serve para decidir quais demonstrações merecem a atenção de uma pessoa.
Uma conta de padaria: a algumas centenas de dólares por problema, o custo de inferência dos 9 problemas de Erdős fica bem abaixo do salário mensal de um pós-doutorando; mas, pelo critério apontado por Curto, quanto o total subiria ao incluir as execuções fracassadas e as chamadas ao AlphaProof, o artigo ainda não informa. A DeepMind já publicou as demonstrações e parte das explicações no repositório alphaproof-nexus-results, no GitHub, para que matemáticos externos possam conferi-las uma a uma.
Fontes: artigo da revista Science, The Decoder, CocoLoop, comentários de especialistas do Science Media Centre da Espanha; o texto do artigo foi conferido quanto aos 9 problemas resolvidos entre 353 de Erdős, às 44 conjecturas provadas entre 492 da OEIS e à divisão de funções das quatro versões de agentes.