O uso de IA está se tornando rotina no site dos problemas de Erdős

• Durante o processo de resolução do problema de Erdős #367, ferramentas de IA desempenharam um papel central, com um caso relatado de colaboração entre matemáticos humanos
• Wouter van Doorn apresentou um contraexemplo gerado por humano para a segunda parte do problema, e depois o Gemini Deepthink gerou uma prova completa da congruência relacionada
• Terence Tao publicou uma versão simplificada da prova baseada em teoria algébrica dos números p-ádicos do Gemini e depois mencionou a possibilidade de formalização em Lean
• Boris Alexeev concluiu a formalização em Lean usando a ferramenta Aristotle, da Harmonic, e verificou manualmente a proposição final para evitar abuso de IA
• Essa sequência de eventos mostra que a assistência de IA na pesquisa matemática está gradualmente se tornando um procedimento padrão

---

Caso de colaboração com IA no problema de Erdős #367

• Em 20 de novembro, Wouter van Doorn apresentou um contraexemplo para a segunda parte do problema, que dependia da suposição de que uma certa congruência fosse verdadeira
  • Ele pediu que outros participantes verificassem a validade dessa congruência
• Algumas horas depois, Terence Tao apresentou a questão ao Gemini Deepthink e, em cerca de 10 minutos, obteve uma prova completa da congruência e a confirmação de todo o argumento
  • A prova do Gemini usou teoria algébrica dos números p-ádicos, e Tao a converteu em uma prova elementar mais simples antes de publicá-la no site
  • Tao comentou que essa prova poderia permitir uma “vibe formalizing” em Lean

Formalização e verificação em Lean

• Dois dias depois, Boris Alexeev concluiu a formalização em Lean usando a ferramenta Aristotle, da Harmonic
  • Para evitar uso indevido de IA, a proposição final foi formalizada manualmente de forma direta
  • Todo o processo levou cerca de 2 a 3 horas, e o resultado foi publicado online
• Depois disso, Tao realizou uma busca bibliográfica com ajuda de IA, mas embora houvesse alguns estudos relacionados, não encontrou nada diretamente ligado ao problema #367

Reação da comunidade e debate

• Alguns usuários acompanham com interesse, por meio das atualizações de Tao, o estado atual do uso de IA na matemática acadêmica
• Outros adotaram uma visão crítica da abordagem formalista do Lean, observando que a compreensão matemática é compressão, enquanto o Lean a decompõe em detalhes de baixo nível
  • O documento relacionado “Against Lean: Why Proof Assistants Formalize the Wrong Thing” argumenta que assistentes de prova como o Lean capturam mal a essência da matemática
• Outro usuário mencionou problemas de precisão nas conversas com IA e avaliou que, embora exija ajuste fino, o uso é agradável

[GN⁺]

Comentários do Hacker News

• É uma experiência incrível poder jogar artigos de ML com foco em matemática para um assistente de IA e receber de volta explicações simples ou pseudocódigo
  Para alguém como eu, que não usava o que aprendeu na universidade há mais de 25 anos, isso ajuda demais

  • Fico curioso sobre como verificar se essa explicação está correta. Definições matemáticas têm muitas sutilezas
  • Acho que esse é exatamente o tipo de situação em que LLMs brilham no aprendizado
    Dá para colocar o artigo no Claude, receber uma visão geral e continuar fazendo perguntas
    Mesmo em áreas como biologia, que eu não estudei na graduação ou no mestrado, consegui me aprofundar como se estivesse conversando com um tutor experiente
  • A notação matemática é altamente dependente de contexto, então, se você pedir para o LLM convertê-la para uma linguagem de baixo contexto como Lisp, fica muito mais rápido entender a estrutura

• Espero que pesquisadores e empresas consigam obter mais ganhos de produtividade na pesquisa científica
  Mesmo um assistente imperfeito já aumenta bastante a alavancagem

  • Existe uma versão beta de um app de formalização para iOS mencionada pelo Tao → Aristotle
    Dizem que é uma startup fundada pelo CEO da Robin Hood

• ‘Vibe formalizing’ parece uma extensão lógica de ‘vibe engineering’ e ‘vibe coding’
  Quando as peças de um problema não se encaixam bem, é interessante uma abordagem tipo ‘Move 37 as a Service’, que combina métodos informais com rigor matemático

  • Já houve um ponto em que travei lendo um artigo sobre polyhedral compilation, e o ChatGPT guiou bem o processo de raciocínio
    Claro, havia partes erradas, mas pude aprofundar meu entendimento conversando e refletindo a minha própria confusão
    A IA é especialmente boa em identificar os pontos em que o usuário está confuso

• Ouvi uma discussão sobre a pronúncia do nome do matemático húngaro Erdős
  No húngaro, a grafia e a pronúncia quase sempre coincidem, mas há exceções nos nomes
  Em inglês, dizem que soa mais ou menos como “airdish”

  • Ő é simplesmente um som de œ (oe). O -y em nomes húngaros é um vestígio do sufixo -i, que indicava linhagem nobre
    Ex.: Görgey, Széchényi, Lánczos etc.
    A ordem dos nomes húngaros, como no japonês, é sobrenome-nome (big endian). Ex.: “Erdős Pál”, “Neumann János”
  • Havia um poema humorístico que vi num mural do departamento de matemática em 1960 — a piada era que um artigo escrito por Erdos refutava o teorema de que ‘o círculo é redondo’
  • Como o significado dos sinais de pronúncia (acentos de pronúncia) varia de idioma para idioma, acho estranho usar sinais húngaros diretamente em frases em inglês
  • No começo, a pronúncia “airdish” me pareceu estranha, mas ao palatalizar a terminação ‘os’, ela passou a soar plausível
  • Como não sou americano, parece que ninguém liga muito para esse tipo de questão de pronúncia

• É interessante notar que há reações com tendência anti-Lean nos comentários

  • Não sou matemático, mas fiquei curioso se esse material anti-Lean é confiável
    Quero saber se é apenas divulgação de uma abordagem diferente ou se existe uma oposição filosófica ao Lean
  • Pessoas conhecidas como o Tao naturalmente atraem muita atenção de excêntricos e teóricos da conspiração

• Os resultados de usar IA em pesquisa matemática foram mistos
  Às vezes ela completa automaticamente argumentos não triviais, mas em certos domínios ela se perde completamente
  Ainda acho que, por enquanto, a IA só é útil como ferramenta de apoio, e não para substituir matemáticos

  • Tive uma experiência parecida. Pedi para ela resolver um problema simples de cálculo de permutações de um artigo, e isso levou mais tempo do que resolver eu mesmo
    Na programação também houve casos em que ela não conseguiu pegar bugs triviais, embora tenha ajudado muito em tarefas complexas
    No fim, essas ferramentas ainda estão longe de substituir especialistas, e o exagero no marketing pode acabar prejudicando a confiança
    Como diz o ditado, ‘se prometeram a lua, precisam entregar a lua’; expectativas realistas são importantes

• Não consigo acreditar que, ainda em vida, cheguei à era de dizer algo como em Star Trek: “Computador, desenhe a prova deste problema de matemática”
  Seria ótimo se “Beam me up, Scotty” também fosse possível

  • Mas se isso significasse morrer toda vez, aí já seria um pouco complicado

• Hoje à noite, enquanto dirigia, conversei com o ChatGPT sobre a estrutura detalhada dos escalonadores de pipeline do LLVM e do GCC
  Isso aumentou muito minha produtividade, e ele organizou automaticamente minhas notas experimentais sobre compiladores
  Era algo inimaginável antigamente

  • Pela minha experiência, é bem provável que o LLM tenha errado parte dos detalhes
    Claro, os resultados podem variar de pessoa para pessoa

• Se derem à IA o nome de Erdos, acho que o número de Erdos de todos nós passaria a ser 1

  • Ou pareceria uma continuação do DR-DOS
  • Na verdade já existe um produto chamado Erdos, um IDE com integração de IA

• Impressiona como ele usou bem as ferramentas de fronteira existentes para criar um ambiente colaborativo de pesquisa matemática

  • Felizmente, a matemática é uma área em que idolatria ou disputa de popularidade não determinam a veracidade dos resultados
    Por isso, ainda considero a matemática uma das raras disciplinas livres de influência pseudocientífica