Alguns problemas matemáticos atravessam gerações sem uma resposta. Dois deles, apresentados em 1970 por Paul Erdős e András Sárközy, agora receberam soluções com a participação de uma inteligência artificial do Google DeepMind. O avanço do AlphaProof Nexus mostra como sistemas automatizados podem contribuir para a pesquisa matemática. Ao mesmo tempo, reforça uma distinção importante: encontrar uma demonstração correta e compreender suas ideias são tarefas relacionadas, mas diferentes.
Uma IA propõe, um verificador confere
O estudo sobre a busca automatizada de demonstrações, publicado na Science, apresenta uma estrutura que utiliza o Gemini 3.1 Pro para desenvolver possíveis soluções.
Essas tentativas passam pelo Lean, uma ferramenta de verificação formal. Quando encontra erros, o sistema recebe informações que ajudam a reformular o raciocínio. Assim, a busca avança por ciclos de elaboração, conferência e revisão.
Na versão mais completa, diferentes agentes exploram caminhos e compartilham tentativas. Um mecanismo de seleção favorece propostas consideradas promissoras, enquanto o AlphaProof pode ajudar a resolver etapas específicas.
Entretanto, a estrutura mais sofisticada não foi indispensável para todos os resultados. Em uma avaliação posterior, a versão básica também resolveu os nove problemas de Erdős, embora com maior custo nos casos difíceis.
O que os números realmente mostram
O sistema resolveu nove dos 353 problemas de Erdős examinados. Também demonstrou 44 das 492 conjecturas analisadas na Enciclopédia On-line de Sequências de Números Inteiros, conhecida como OEIS.
Uma conjectura é uma afirmação considerada plausível, mas que ainda precisa de demonstração. Nesse contexto, a contribuição da IA vai além de calcular exemplos: ela produz um argumento formal para sustentar o resultado.
A Universidade de Aarhus, que participou da pesquisa, destaca que o matemático Gergely Bérczi ajudou a identificar problemas adequados, validar soluções e escrever versões das demonstrações em linguagem natural.
O sistema também contribuiu para trabalhos em geometria algébrica, otimização, teoria dos grafos e óptica quântica. Ainda assim, os números deixam claro que a maioria das questões avaliadas permaneceu sem solução.
Uma prova verificada ainda precisa de interpretação
A verificação formal oferece uma vantagem importante: cada passo deve obedecer às regras do ambiente matemático utilizado. Isso permite conferir demonstrações extensas sem depender apenas da leitura humana.
Mas existe uma etapa anterior igualmente decisiva. O enunciado inserido no programa precisa representar corretamente o problema original. Uma prova impecável de uma afirmação diferente não resolve a questão pretendida.
Por isso, os pesquisadores verificaram se as formulações dos problemas solucionados correspondiam às conjecturas originais. A orientação humana também aparece na escolha das perguntas e no conhecimento adicional fornecido ao sistema.
As demonstrações estão abertas à conferência
O repositório público de resultados do AlphaProof Nexus reúne as provas em Lean e versões explicativas de parte delas. O material inclui instruções para verificar as demonstrações e referências às fontes das conjecturas.
Há uma distinção relevante nessa organização: as provas formais foram produzidas pelo sistema, enquanto os textos em linguagem natural foram escritos por pessoas seguindo sua estrutura.
Essa passagem para uma explicação legível ajuda outros matemáticos a examinar as ideias, reconhecer conexões e utilizar os resultados em pesquisas futuras. O repositório também disponibiliza informações sobre os problemas tentados, permitindo contextualizar os sucessos.
O avanço aponta para uma colaboração em que a máquina amplia a busca por soluções e os pesquisadores dão direção e significado ao trabalho. A resposta correta é uma conquista; transformá-la em conhecimento que outras pessoas possam compreender continua sendo parte essencial da matemática.
