📸 Créditos da imagem: Unsplash
Certos desafios matemáticos desafiam o intelecto humano por décadas sem que ninguém encontre um caminho definitivo para sua resolução. Esse era o caso de dois problemas célebres propostos em 1970 pelos matemáticos Paul Erdős e András Sárközy, que permaneceram sem resposta por mais de 50 anos até receberem soluções formais com o auxílio do sistema AlphaProof Nexus, desenvolvido pela equipe do Google DeepMind.
O avanço demonstra a capacidade crescente de ferramentas automatizadas de raciocínio lógico em contribuir ativamente com a pesquisa matemática avançada. Mais do que apenas apresentar resultados, o feito destaca uma fronteira essencial na disciplina: a diferença entre construir uma demonstração tecnicamente correta e assimilar em profundidade os conceitos matemáticos que a tornam possível.
Uma IA propõe, um verificador confere
O método por trás da descoberta foi detalhado em um estudo publicado na revista Science e fundamenta-se em uma arquitetura híbrida. O modelo Gemini 3.1 Pro é empregado para propor caminhos e rascunhar possíveis resoluções, enquanto o Lean, um renomado assistente de provas e ferramenta de verificação formal, audita cada etapa lógica com rigor absoluto.
Sempre que o verificador encontra inconsistências ou falhas de raciocínio, o sistema recebe diagnósticos detalhados que servem como guia para reformular a abordagem. A busca por uma demonstração válida ocorre, dessa forma, por meio de ciclos sucessivos de formulação, checagem e revisão. Em sua configuração mais completa, múltiplos agentes computacionais atuam em paralelo, compartilhando progressos para que os caminhos mais promissores sejam priorizados, com o suporte do AlphaProof em etapas complexas. A versão básica do sistema também conseguiu solucionar os problemas, embora tenha demandado um esforço computacional significativamente superior nos casos difíceis.
O que os números realmente mostram
Para mensurar o impacto e a eficiência da metodologia, os pesquisadores colocaram o sistema à prova diante de extensos catálogos de conjecturas em aberto. Os resultados obtidos incluíram:
- A resolução de 9 dos 353 problemas examinados formulados por Paul Erdős;
- A demonstração de 44 das 492 conjecturas analisadas da Enciclopédia On-line de Sequências de Números Inteiros (OEIS).
Na matemática, uma conjectura representa uma hipótese fundamentada e plausível, mas que carece de uma prova conclusiva. Nesse cenário, o trabalho desempenhado pela inteligência artificial não se resumiu a testar números ou calcular exemplos numéricos exaustivamente: o sistema formulou argumentos lógicos formais e completos para validar cada enunciado.
O projeto contou com a colaboração de pesquisadores da Universidade de Aarhus. O matemático Gergely Bérczi teve papel fundamental na identificação de questões adequadas para o experimento, na validação dos resultados e na posterior transcrição das provas formais para a linguagem matemática tradicional. Além da teoria dos números, a tecnologia prestou suporte a estudos em geometria algébrica, problemas de otimização, teoria dos grafos e óptica quântica, ainda que a esmagadora maioria dos enigmas testados tenha continuado sem solução.
Uma prova verificada ainda precisa de interpretação
O uso de ferramentas de verificação formal como o Lean traz a segurança de que nenhuma premissa foi violada e que cada dedução atende estritamente aos axiomas do sistema. Esse recurso permite auditar demonstrações gigantescas sem depender unicamente da revisão visual feita por pares, que muitas vezes pode deixar passar detalhes sutis.
Apesar dessa precisão computacional, a intervenção humana permanece indispensável. Uma das etapas mais críticas consiste em traduzir com total fidelidade o enunciado original para a sintaxe do verificador formal. Demonstrar uma afirmação irrepreensível, mas com ligeiras divergências do postulado de origem, invalidaria o feito. Por essa razão, os pesquisadores revisaram rigorosamente se cada problema traduzido correspondia com exatidão à conjectura matemática pretendida.
As demonstrações estão abertas à conferência
Para assegurar a transparência científica e permitir o escrutínio da comunidade acadêmica, todos os resultados do AlphaProof Nexus foram disponibilizados em um repositório público. A plataforma inclui os códigos das provas em Lean, instruções de reprodução e referências às fontes de cada conjectura.
O material também disponibiliza versões explicativas redigidas em linguagem natural por especialistas humanos a partir da estrutura dedutiva criada pela máquina. Esse processo de tradução é crucial para que a comunidade matemática possa estudar os novos métodos, conectar os achados a outras áreas do conhecimento e incorporar as lições em futuras pesquisas. A experiência consolida um modelo colaborativo onde os computadores ampliam exponencialmente a escala de busca por deduções lógicas, enquanto os cientistas fornecem o direcionamento, o rigor interpretativo e o significado às descobertas.
📰 Leia a notícia completa em: Gizmodo »