Google resolve nove problemas matemáticos inéditos com IA e acelera corrida por descobertas científicas

A disputa entre gigantes da inteligência artificial (IA) acaba de atingir um novo patamar — e agora envolve alguns dos problemas matemáticos mais difíceis do mundo. A Google DeepMind anunciou que seu sistema AlphaProof Nexus conseguiu resolver nove problemas abertos atribuídos ao lendário matemático húngaro Paul Erdős, incluindo dois que permaneciam sem solução havia 56 anos.

O avanço foi divulgado em um novo artigo científico publicado no arXiv e chega apenas um dia após a OpenAI revelar que sua própria IA havia derrubado uma conjectura matemática relacionada a Erdős. O episódio marca uma nova fase da corrida tecnológica: modelos de IA deixando de apenas responder perguntas para produzir descobertas matemáticas inéditas e verificáveis.

O AlphaProof Nexus combina grandes modelos de linguagem (LLMs) com o Lean, um sistema de verificação formal de provas matemáticas. Em vez de apenas sugerir soluções plausíveis, a IA gera demonstrações completas que são checadas automaticamente pelo software até que uma delas seja validada sem ambiguidades.

Segundo os pesquisadores, o sistema solucionou problemas ligados à combinatória e teoria dos grafos — áreas fundamentais da matemática moderna e extremamente relevantes para computação, criptografia e ciência de redes. Além disso, a IA também demonstrou 44 conjecturas abertas presentes na Online Encyclopedia of Integer Sequences (OEIS), uma das maiores bases matemáticas do mundo.

O mais impressionante é o custo relativamente baixo do processo. De acordo com a equipe da DeepMind, cada problema resolvido consumiu apenas algumas centenas de dólares em computação. Isso sugere que sistemas desse tipo podem futuramente se tornar ferramentas acessíveis para universidades, laboratórios e centros de pesquisa.

Os cientistas explicam que o modelo funciona em ciclos iterativos. Primeiro, o LLM propõe caminhos matemáticos possíveis. Em seguida, o Lean verifica rigorosamente cada etapa da prova. Caso encontre inconsistências, o sistema retorna ao início e tenta novas abordagens até obter uma demonstração formalmente correta.

Esse mecanismo representa uma mudança importante em relação a muitos sistemas atuais de IA generativa, frequentemente criticados por “alucinações” ou erros factuais. Na matemática formal, não há espaço para respostas aproximadas: a prova precisa ser perfeita.

Apesar do avanço, os próprios pesquisadores admitem que ainda existem limites importantes. Problemas que exigem construções matemáticas totalmente novas ou intuições muito abstratas continuam fora do alcance da IA. Em muitos casos, o sistema ainda depende de estruturas conceituais já conhecidas por matemáticos humanos.

Mesmo assim, especialistas consideram o resultado um marco histórico. Resolver problemas abertos por décadas — especialmente ligados ao legado de Erdős — é algo extremamente raro mesmo entre matemáticos profissionais. O pesquisador publicou mais de 1.500 artigos ao longo da vida e deixou centenas de desafios famosos, muitos acompanhados de recompensas financeiras informais.

A notícia também reforça a crescente importância da chamada “verificação formal”, técnica que vem ganhando espaço tanto na matemática quanto na engenharia de software. Em vez de confiar apenas na revisão humana, sistemas como Lean conseguem validar logicamente cada passo de uma demonstração matemática, reduzindo drasticamente a chance de erros.

Nos bastidores, a disputa entre Google e OpenAI parece estar acelerando o desenvolvimento desse tipo de ferramenta. Na semana passada, a OpenAI afirmou que seu modelo conseguiu refutar uma conjectura de Erdős que existia havia 80 anos — meses após recuar de uma alegação anterior de ter resolvido dez problemas matemáticos inéditos.

A movimentação mostra que a matemática se tornou um novo campo estratégico para empresas de IA. Diferentemente de benchmarks tradicionais, problemas matemáticos abertos oferecem uma maneira concreta de medir raciocínio original, criatividade lógica e capacidade de descoberta científica.

Mais do que resolver exercícios acadêmicos, essas tecnologias podem ter impactos profundos em áreas como física, biologia, engenharia, segurança digital e desenvolvimento de novos materiais. Muitos avanços científicos dependem justamente da formulação — e prova — de estruturas matemáticas complexas.

O que antes parecia ficção científica começa a se transformar em realidade: inteligências artificiais atuando como colaboradoras científicas capazes de acelerar descobertas em velocidade inédita. E, ao que tudo indica, a corrida pelas próximas grandes provas matemáticas está apenas começando.

Leia também: