Problema de Erdős #728 é resolvido de forma quase autônoma por IA

• O problema de Erdős #728 foi recentemente resolvido de forma quase autônoma por ferramentas de IA, marcando um novo marco na automação da pesquisa matemática
• O problema era originalmente uma questão sobre a fatoração em primos de coeficientes binomiais proposta por Erdős, Graham, Ruzsa e Strauss em 1975, e por conta de condições ambíguas ficou por muito tempo sem tratamento claro
• O ChatGPT gerou uma prova sob restrições ajustadas, e o Aristotle a formalizou como uma prova formal em Lean, corrigindo erros automaticamente
• Depois, vários participantes reescreveram em linguagem natural com o ChatGPT e melhoraram iterativamente versões com conexões com a literatura e uma estrutura narrativa mais forte
• Terence Tao avaliou que esse processo mostra o potencial da capacidade da IA de redigir e revisar provas rapidamente para mudar a própria forma de escrever artigos de pesquisa

---

O problema de Erdős #728 resolvido por IA

• Recentemente, a aplicação de ferramentas de IA trouxe novo avanço à resolução de problemas de Erdős, e o problema #728 foi resolvido de forma quase autônoma por IA
  • Após uma tentativa inicial, a versão revisada com base no feedback teve sucesso
  • O resultado não foi reproduzido da mesma forma na literatura existente, havendo apenas resultados semelhantes por métodos parecidos
• Esse caso mostra que, nos últimos meses, a capacidade da IA para resolver problemas matemáticos realmente melhorou
  • Já havia casos no passado em que IA resolveu problemas de Erdős, mas a maioria depois se mostrou corresponder a soluções já existentes na literatura
• Neste caso, a formulação original de Erdős havia sido apresentada de forma incorreta e só recentemente foi reconstruída na forma pretendida
  • Isso ajuda a explicar por que havia pouca pesquisa relacionada na literatura existente

História do problema e abordagem inicial

• Em 1975, Erdős, Graham, Ruzsa e Strauss estudaram a fatoração em primos do coeficiente binomial (2n choose n) e propuseram vários problemas relacionados
  • Um deles perguntava se existiam infinitos valores de a, b e n que satisfizessem a condição a!b! | n!(a+b−n)! e a+b > n + C log n
  • No entanto, várias partes foram descritas de forma pouco clara, inclusive o tamanho de C (se pequeno ou grande)
• Há alguns meses, a equipe do AlphaProof encontrou uma solução simples para o problema, mas como ela não correspondia ao espírito pretendido da questão, foi adicionada a restrição a,b ≤ (1−ε)n
  • Depois disso, mesmo com busca bibliográfica assistida por IA, quase não foram encontrados trabalhos relacionados

Colaboração entre ChatGPT e Aristotle

• Em 4 de janeiro, o ChatGPT gerou uma prova para o caso de C pequeno sob as restrições ajustadas
  • Essa prova foi formalizada pelo Aristotle como uma prova formal em Lean
  • Depois, ao reexaminar o texto original, confirmou-se que o artigo original já tratava do caso de C pequeno
• Outro participante converteu a prova em Lean em linguagem natural com o ChatGPT e, por meio de conversas adicionais, produziu uma versão aprimorada
  • Essa versão preencheu algumas lacunas da prova, mas ainda mantinha um estilo estranho típico de IA e falta de referências bibliográficas
  • Mesmo assim, chegou a um nível legível o suficiente para que se pudesse entender a ideia central

Reescrita em grande escala e resultado aprimorado

• Com prompts adicionais, o ChatGPT gerou uma prova estendida também para o caso de C grande
  • Havia alguns erros, mas o Aristotle os corrigiu automaticamente e concluiu uma prova verificada em Lean
• Depois que um terceiro participante comprimiu a prova em Lean, outro participante, por meio de uma longa conversa com o ChatGPT,
  • a reescreveu na forma de um artigo mais acabado, com conexões com a literatura e uma estrutura narrativa reforçada
  • O resultado foi avaliado como tendo menos aparência de conteúdo gerado por IA e qualidade próxima ao nível de um artigo de pesquisa
  • Tao mencionou que revisou esse texto no fórum de problemas de Erdős

Como a IA está mudando a escrita de artigos de pesquisa

• Tao considera que, no artigo final, as partes centrais ainda precisam ser escritas por humanos, mas
  • avalia que a combinação de IA e Lean aumentou drasticamente a velocidade de redação e revisão de provas
• Antes, levava-se muito tempo para tornar um artigo agradável de ler,
  • e revisões com base no feedback de pareceristas muitas vezes se limitavam a mudanças localizadas
• Agora, porém, a capacidade de geração e edição de texto da IA combinada com a função de verificação das ferramentas de prova formal
  • permite gerar rapidamente novas versões de um artigo com diferentes níveis de precisão e estilos de exposição
• Além de um “artigo oficial”, pode haver muitas versões auxiliares geradas por IA,
  • levantando a possibilidade de oferecer diferentes perspectivas e valor adicional

Reação da comunidade

• Alguns usuários descreveram o valor adicional de documentos gerados por IA como a “capacidade de enxergar por outro ângulo”
• Outros matemáticos levantaram a necessidade de medir a originalidade dos resultados da IA ou avaliar a semelhança com a literatura existente
  • Por exemplo, foi proposta uma medição quantitativa de similaridade por meio da comparação do comprimento de provas formais em Lean
• Outro comentário observou que a IA pode reescrever artigos globalmente, como em refatoração de código,
  • de modo que pesquisadores deveriam se concentrar mais no projeto da estrutura do documento em alto nível
• Alguns reagiram com ceticismo à possibilidade de a IA substituir o papel do matemático,
  • enquanto outros avaliaram isso como uma nova oportunidade de colaboração e expansão do pensamento

[GN⁺]

Comentários no Hacker News

• Trabalho na Harmonic e quero corrigir alguns mal-entendidos sobre o Aristotle que criamos
  O Aristotle usa ativamente técnicas modernas de IA, incluindo modelagem de linguagem
  Se você inserir uma prova informal em inglês, há uma alta probabilidade de que ele a traduza para Lean caso a prova esteja correta. Ou seja, isso serve como um forte sinal de que a prova em inglês é sólida
  Depois que ela é formalizada em Lean, não há dúvida de que a prova está correta. Essa é a nossa abordagem central — se encontrarmos a resposta por meio de exploração orientada por IA, podemos garantir a correção do resultado independentemente da complexidade

  • Tenho curiosidade sobre como vocês verificam se a prova traduzida pela IA para Lean é realmente a formalização correta do problema. Em outras áreas, IA generativa é muito boa em produzir mentiras plausíveis, então queria saber se isso também pode acontecer aqui
  • Tenho curiosidade se há tentativas de aplicar essa tecnologia à verificação de software
    O Rust usa um conjunto fixo de regras para garantir segurança de memória, mas essas regras são simples e limitadas. Seria muito legal se um sistema como o Aristotle pudesse ser integrado ao compilador, permitindo passar automaticamente quando fosse possível uma prova de correção do código
  • Sempre que usam um novo LLM, fico em dúvida se é progresso real ou só hackeamento de benchmark, mas acho que a formalização de provas matemáticas é um indicador de avanço de verdade
    Quanto tempo deve levar para a Harmonic conseguir formalizar a maior parte da matemática escrita por humanos? O concorrente Christian Szegedy disse que isso seria possível ainda este ano
  • Você disse que, quando a prova em inglês está correta, há alta probabilidade de tradução para Lean; tenho curiosidade se isso varia conforme a dificuldade por área da matemática. Pelo que sei, ainda há muitas áreas de pesquisa que até humanos têm dificuldade de formalizar
  • A premissa “se a proposição foi formalizada corretamente” parece uma suposição bem forte. Como vimos recentemente no caso Navier-Stokes, a própria formalização não é fácil

• Pela explicação de Terence Tao, parece que um humano ficou passando resultados entre duas ferramentas de IA, e a IA teve o papel de preencher lacunas encontradas pelo humano
  Parece mais uma colaboração entre humano e IA do que uma solução totalmente autônoma. Ou seja, o especialista lidera e a IA auxilia

  • Sim, entendo que na prática foi um processo de interação entre o Aristotle, o ChatGPT e um usuário muito habilidoso
  • Pelo que ouvi, não foi o Tao nem a comunidade que encontraram as lacunas diretamente, e sim um verificador automático de provas. Na verdade, parece algo mais próximo de IA 90% / humano 10%
  • Há uma explicação detalhada do autor no Reddit — post no Reddit
  • Para entender o nível de expertise e esforço humano envolvido, recomendo ler a thread no fórum de problemas de Erdős
  • Como curiosidade, esse site foi criado pelo matemático Thomas Bloom, e o ChatGPT ajudou na configuração técnica (citação do FAQ)

• Reestruturar provas existentes ou combiná-las de novas maneiras é um processo tedioso ou complexo para humanos, mas a IA pode fazer isso em velocidade sobre-humana
  Essa abordagem deve abrir um enorme potencial mesmo antes da AGI. Parece que está chegando a era em que matemáticos usarão IA como ferramenta para lidar com desafios como os Problemas do Milênio

  • Acho que não há uma fronteira clara entre reestruturar provas existentes e criar matemática completamente nova
  • Como a matemática é lógica, imagino que já existam muitos algoritmos para esse tipo de exploração, então não me parece um simples problema de busca
  • Também concordo com a parte de reestruturar provas existentes. Verificar o que o LLM produz ainda é um trabalho tedioso, mas ainda assim melhor do que fazer tudo manualmente
    O verdadeiro valor dos LLMs está em oferecer novas perspectivas sobre temas que podem ser expressos em linguagem
  • Chamo esse fenômeno de “refatoração científica”. Por exemplo, a IA passa a conseguir fazer automaticamente experimentos como trocar uma constante e refazer toda a lógica
  • Se uma IA capaz de provar teoremas complexos não for AGI, então fico me perguntando o que seria AGI

• No texto explicativo escrito por quem realmente resolveu o problema, chama atenção o fato de que o resultado foi obtido com apenas alguns prompts, sem um pipeline gigantesco
  Os modelos recentes usam muito mais recursos computacionais, então isso parece mais um resultado de piso do que de teto

• Terence Tao criou uma página wiki chamada “AI contributions to Erdős problems”
  Pela página no GitHub e pela postagem no Mathstodon, este resultado (problema 728) é o primeiro “item verde” da página, ou seja, o primeiro caso realmente resolvido por IA

  • Curiosamente, a maioria das provas formalizadas por IA na seção 6 da wiki foi concluída nos últimos meses. O futuro parece promissor

• Tenho curiosidade se especialistas em áreas complexas como física ou matemática também conversam com IA e recebem ajuda

  • Tenho doutorado em matemática pura e hoje trabalho como cientista de dados. A IA ajuda muito em revisão de literatura ou para revisar rapidamente matemática com a qual não estou familiarizado
    Por área, a utilidade cai na ordem: programação > ML aplicado > estatística/matemática aplicada > matemática pura
  • Não sou da área de física, mas graças à IA o tempo que gasto procurando fórmulas ou artigos diminuiu muito. Ainda assim, sempre preciso verificar os resultados
  • Do ponto de vista de quem pesquisa modelos de deep learning e novas estruturas de attention, o ChatGPT é muito útil para busca de artigos e exploração de ideias relacionadas
  • Como alguém que faz matemática por hobby, os LLMs me dão feedback sobre minhas tentativas ou me encaminham para soluções existentes. Para a matemática como brincadeira, é uma ferramenta bem divertida
  • Trabalho com pesquisa em geometria algébrica e, fora busca bibliográfica, ainda não tive muita ajuda. Há bastante variação entre modelos

• Já dá para usar o Aristotle agora mesmo — https://aristotle.harmonic.fun/

  • Também tenho curiosidade se testam a IA com o dataset formal-conjectures da DeepMind
  • Na documentação está “uvx aristotlelib@latest aristotle”, mas na verdade o correto é “uvx --from aristotlelib@latest aristotle”
    Além disso, o link para a página pessoal de Stanford está errado (é preciso remover o www)
  • Isso é interessante o suficiente para merecer uma thread separada no HN. Se eu fosse o CEO, talvez publicasse um post de apresentação diretamente (link de referência)

• Este resultado é um teorema sobre inteiros, uma área em que a infraestrutura do Mathlib oferece bom suporte
  As definições usadas também não são complexas, então esse tipo de prova tem alta probabilidade de sucesso. Ainda assim, é uma conquista realmente impressionante

• Este é um exemplo que mostra o potencial de uma abordagem de IA especializada além dos LLMs
  O artigo do Aristotle está em arXiv:2510.01346
  Só porque usa arquitetura Transformer não significa que tudo seja LLM — se não for treinado com dados de linguagem, não dá para chamar de LLM

  • Parece que muita gente usa “LLM” e “GenAI” como se fossem sinônimos, e isso gera confusão
  • Você disse “abordagem que vai além de LLM”, mas na prática não foi usado o ChatGPT?
  • Sim, na prática o ChatGPT foi usado
  • Pelo artigo, os três estágios envolvem LLMs grandes baseados em Transformer
    1. Na Monte Carlo Graph Search, atuando como função de política/valor
    2. No sistema de raciocínio informal, usando chain of thought
    3. O AlphaGeometry também usa um modelo de linguagem neuro-simbólico
       Ou seja, todas as etapas são baseadas em LLM

• Em 2026, acho que a IA vai lidar com cada vez mais problemas em aberto da matemática
  Este caso também não foi totalmente autônomo, mas chegou perto de a IA resolver sozinha depois do feedback humano
  Acho que o debate de que “LLMs são apenas papagaios estocásticos” acabou. Daqui para frente, a verdadeira discussão vai ser como colocar isso em uso prático

  • Em 2026, acho que veremos avanços explosivos na matemática
  • Este resultado provavelmente é um remix de provas semelhantes que estavam nos dados de treinamento, mas essa capacidade de remix por si só já é poderosa
  • Ainda é necessária verificação independente. É difícil confiar apenas na alegação de uma empresa