IA Aristotle resolve enigma de Erdős… mas trivial

A startup Harmonic, de Vlad Tenev, alega que sua IA Aristotle resolveu o Problema #124 de Erdős. A prova foi verificada em Lean.

• Resolução em 6 horas, mas de versão alternativa que permite o número 1.
• Problema original (sem 1) segue aberto desde 1995.
• Críticas: marketing exagerado e solução possivelmente de dados de treino.

A startup Harmonic, fundada pelo ex-CEO do Robinhood Vlad Tenev, anunciou em 28 de novembro de 2025 que sua IA Aristotle resolveu o Problema #124 de Erdős. O feito ocorreu em 6 horas, com prova verificada pelo sistema formal Lean em 1 minuto.

O problema, proposto em 1995 no artigo ‘Complete sequences of sets of integer powers’, questiona se certos conjuntos de bases numéricas podem representar todos os números naturais como somas de potências distintas maiores que 1, sob a condição ∑ 1/(d_i – 1) ≥ 1.

A Solução da Aristotle e o Erro Conceitual

A prova, publicada no GitHub da Harmonic, aborda uma versão alternativa que permite potências d_i^0 = 1. Matemático Boris Alexeev, afiliado à Harmonic e Princeton, configurou o problema assim.

No fórum oficial do Projeto Erdős, especialistas esclarecem: a versão original exclui o 1, tornando-a não trivial. A de Aristotle é ‘um exercício de olimpíada’, resolvível por representações em bases com dígitos {0,1}.

Críticas da Comunidade Técnica

Discussões no Hacker News e Mathstodon destacam:

• A solução usa táticas padrão do Lean, como linarith e ring, sem inovação.
• Provável presença nos dados de treino da IA, invalidando ‘descoberta autônoma’.
• Termo ‘vibe proving’, de Tenev, ignora rigor matemático.

Alexeev admite: Aristotle resolveu ‘a’ versão, não ‘a’ original. O problema de 30 anos segue aberto.

Contexto Comercial e Riscos

O anúncio surge antes de rodada de investimentos da Harmonic, que busca pioneirismo em IA matemática. Críticos alertam para hype excessivo, risco de desinformação e pressão por resultados rápidos em pesquisa rigorosa.

Matemáticos enfatizam: LLMs recombinam conhecimento existente, mas falham em criatividade para enigmas como Collatz ou Riemann.