Matemáticos humanos são ultrapassados por IA na busca de contraexemplos

• Modelos das famílias ChatGPT e Claude produziram, em poucas semanas, contraexemplos para a conjectura da distância unitária de Erdős, a questão de esquemas de grupos de Grothendieck e a Jacobian Conjecture, com alguns deles verificados em Lean
• O Sol, da OpenAI, formalizou em 3 semanas o contraexemplo de Erdős e os resultados necessários de teoria global dos corpos com 1,2 milhão de linhas de código Lean, mais da metade das 2,3 milhões de linhas do mathlib escritas ao longo de 9 anos
• Para a pergunta de 60 anos de Grothendieck, o Sol encontrou um contraexemplo de 12 páginas e o Fable o formalizou em 1.076 linhas em 4 horas, confirmando a existência de um esquema de grupos de ordem 4, mas não aniquilado por 4
• A formalização automática também acelerou muito o ritmo da pesquisa: Andrew Yang escreveu cerca de 250 mil linhas de código Lean em aproximadamente 2 semanas, praticamente concluindo o projeto do teorema de elevação de modularidade necessário para o último teorema de Fermat
• Não dá para confiar cegamente na matemática informal gerada por IA, mas, ao transformar uma conjectura em uma proposição exata em Lean, é possível verificar mecanicamente provas e refutações, e cabe aos humanos extrair insights matemáticos mais profundos dos contraexemplos

---

A conjectura da distância unitária de Erdős e a teoria global dos corpos

• Em 20 de maio de 2026, o ChatGPT refutou a conjectura da distância unitária de Erdős, da geometria discreta
  • O contraexemplo foi construído usando um profundo teorema de teoria dos números de Golod e Shafarevich, dos anos 1960
  • Vários matemáticos revisaram o argumento antecipadamente e o consideraram válido, mas no momento da divulgação não havia formalização em Lean
• Em 26 de maio, o medalhista Fields Mike Freedman, cientista-chefe da Logical Intelligence, informou que seu sistema havia formalizado automaticamente em Lean todo o artigo do ChatGPT
  • O escopo da formalização era a proposição de que o teorema de Golod–Shafarevich implica o contraexemplo de Erdős
  • O próprio teorema de teoria dos números em que tudo se apoia exige mais de 100 páginas e depende de uma grande parte da teoria global dos corpos
• Durante o ano após a escola de verão de formalização da teoria dos corpos de 2025, o caso local ficou quase concluído, mas o caso global permaneceu em aberto

A formalização completa de 1,2 milhão de linhas feita pelo Sol

• Em 26 de junho, Boris Alexeev, da OpenAI, publicou no Lean Zulip que guiou o novo modelo Sol para produzir uma formalização completa do contraexemplo de Erdős sem assumir nada além dos axiomas da matemática
• O Sol gerou 1,2 milhão de linhas de código Lean em 3 semanas
  • O mathlib, escrito ao longo de 9 anos, tem 2,3 milhões de linhas
  • A qualidade do código era irregular, mas ele de fato provava resultados difíceis de teoria global dos corpos e teoremas não triviais sobre cohomologia de corpos numéricos
• Como o Lean é uma linguagem de programação capaz de executar comandos arbitrários, o código gerado foi executado em sandbox por causa do risco de código malicioso
• Essa escala e velocidade levaram à conclusão de que o desenvolvimento matemático gerado por IA em larga escala é inevitável

Workshop Formalizing Fermat e acessibilidade das ferramentas

• O workshop Formalizing Fermat, realizado de 6 a 10 de julho, teve 25 participantes, mas o sistema de formalização automática da patrocinadora Logos Research só podia ser usado por 5 pessoas ao mesmo tempo
• Todos os participantes receberam uma assinatura Claude Max de um mês para poder usar o Claude Fable, e a OpenAI também ofereceu gratuitamente um mês de acesso ao ChatGPT Pro
  • O Sol estava previsto para ser lançado em 9 de julho
  • O Fable deveria ser encerrado em 7 de julho, mas o acesso foi mantido na prática
  • Os participantes puderam usar Sol e Fable em 4 dos 5 dias do workshop e as ferramentas da Logos durante todo o período
• Para desenvolver a teoria de esquemas de grupos finitos e planos necessária para a formalização do último teorema de Fermat, artigos clássicos foram inseridos no Fable e no ChatGPT para gerar explicações em linguagem natural
  • A Logos encontrou que uma proposição incluída na explicação era falsa e apresentou um contraexemplo explícito
  • Após a verificação, constatou-se que o documento gerado por LLM descrevendo uma construção padrão estava errado, e os humanos deixaram passar o erro durante a leitura
  • A diferença foi que, em vez de simplesmente responder que não entendia o argumento, o sistema forneceu uma prova de que o argumento estava errado

A questão de esquemas de grupos de Grothendieck

• O professor Akhil Mathew, da UChicago, propôs à IA a antiga questão de Grothendieck sobre se todo esquema de grupos finito livre de ordem (n) é aniquilado por (n)
  • Deligne provou o caso comutativo
  • Grothendieck provou o caso em que a base é reduced
  • Rene Schoof tratou de mais casos, e Emiliano Torti também provou um caso mais geral em um artigo do ano anterior
• No dia seguinte ao workshop, em 11 de julho, o Sol encontrou um contraexemplo e gerou um PDF de 12 páginas
  • Quando se pediu a formalização completa em Lean em vez de um resultado informal, o Fable a produziu automaticamente em 1.076 linhas em 4 horas
• O arquivo Lean foi primeiro inspecionado para confirmar que continha apenas teoremas, sem comandos como exclusão de arquivos, e então compilado em um notebook
  • Foi verificado se a proposição usava apenas conceitos do mathlib
  • Foi conferido se a proposição realmente expressava a existência de um contraexemplo
  • Foi testado se a prova compilava normalmente
  • Toda a verificação levou menos de 5 minutos
• A verificação confirmou a existência de um esquema de grupos de ordem 4, mas não aniquilado por 4
• Akhil Mathew submeteu esse contraexemplo como PR no mathlib
• Enquanto o contraexemplo de Erdős tinha cerca de 1 milhão de linhas, o de Grothendieck tinha cerca de 1.000 e era muito mais simples, mas ainda assim foi um caso em que uma máquina resolveu uma questão de álgebra geométrica com 60 anos

Reações de especialistas e o teorema de elevação de modularidade

• Em 14 de julho, um professor do Imperial College avaliou que o fato de o contraexemplo de Grothendieck ter sido encontrado com facilidade apenas mostra que os humanos não haviam pensado no problema por tempo suficiente
• O doutorando Andrew Yang usou Sol e Fable ao formalizar em Lean o teorema de elevação de modularidade, importante para o último teorema de Fermat
  • Ele escreveu cerca de 250 mil linhas de código Lean em aproximadamente 2 semanas
  • Com isso, praticamente concluiu o projeto
• Outro professor do Imperial considerava difícil entender por que pós-graduandos pagariam US$ 200 por mês por Sol e Fable, mas, depois de ver esses resultados, passou a achar irracional que um doutorando não gastasse US$ 200 por mês com essas ferramentas
• Harvard já oferecia acesso gratuito ao Fable para todos os seus doutorandos, pós-doutorandos e professores

Contraexemplo para a Jacobian Conjecture

• Akhil Mathew e Levent Alpöge discutiram maneiras de encontrar mais contraexemplos em álgebra geométrica, e o Fable encontrou um contraexemplo para a famosa Jacobian Conjecture, um problema em aberto havia cerca de 100 anos
• Levent Alpöge publicou no X um resultado que parecia ter sido resolvido durante a final da Copa do Mundo de 2026
• Quando Akhil Mathew propôs um novo PR para o mathlib, Paul Lezeau já havia formalizado manualmente o contraexemplo e enviado um PR para o repositório Formal Conjectures, da DeepMind
• O mathlib não tem uma grande lista de conjecturas matemáticas, mas o repositório Formal Conjectures tem
• Se os humanos concordarem sobre uma proposição em Lean que capture fielmente o significado da conjectura, então se torna simples verificar se o código gerado por IA prova ou refuta essa conjectura

O que resta aos humanos após a verificação formal

• No caso da Jacobian Conjecture, o próximo passo para os humanos é entender exatamente o que está acontecendo naquele contraexemplo
• No contraexemplo de Grothendieck, também está em andamento um esforço para ir além de uma listagem de representações arbitrárias de anéis e cálculos e alcançar uma compreensão mais profunda
• O valor de um contraexemplo não se limita a encerrar formalmente um problema; ele se completa no processo de extrair insights que ajudem os humanos a compreender melhor a matemática

[GN⁺]

Opiniões no Hacker News

• Na pós-graduação, tive a oportunidade de contribuir diretamente para um problema em aberto em uma aula de pesquisa do meu orientador. Em uma sexta-feira, o professor apresentou uma conjectura suave e bonita que ele esperava que fosse verdadeira, mas eu, que gostava de exceções estranhas e também não tinha ferramentas de prova suficientes, foquei em encontrar um contraexemplo e o encontrei em uma hora.
  O professor passou o fim de semana inteiro sem conseguir prová-la, e isso mostrou que pessoas com ferramentas, expectativas e motivações diferentes podem contribuir em direções completamente distintas ao olhar para o mesmo problema. Eu não podia me comparar ao meu grande orientador, mas naquele momento eu tinha motivo para olhar em outra direção, e isso levou a um pequeno contraexemplo, minha única contribuição à pesquisa matemática.

  • Talvez seja por isso que máquinas sejam boas em encontrar contraexemplos. Elas não têm fixação estética por conjecturas nem vergonha de apresentar resultados feios.
  • Como matemático, minha percepção é a oposta. Para uma prova, basta modificar um pouco uma prova conhecida, mas para construir um contraexemplo é preciso entender profundamente a estrutura do objeto, algo que muitas vezes está além da minha capacidade.
    Dito isso, talvez isso aconteça porque trabalho sobretudo com objetos abstratos difíceis de entender, e é bem possível que o oposto valha para números ou polinômios.
  • Professores, pesquisadores e docentes que expõem aos alunos problemas ainda não resolvidos e os convidam a participar deveriam ser mais valorizados. Na minha primeira aula de engenharia na universidade, quando o instrutor disse aos calouros: “estes são problemas que ainda não conseguimos resolver; se tiverem alguma ideia, nos avisem”, eu me senti mais acolhido e incluído na comunidade do que nunca, e isso foi uma grande inspiração no início dos estudos, que poderia ter sido tedioso.
  • Há uma história quase igual em 《How to Solve It》.
  • Há uma anedota mais extrema e na direção oposta sobre Zeeman. Ele passou anos tentando encontrar uma esfera enlaçada em um espaço de 5 dimensões, até perceber que isso era impossível e prová-lo em poucas horas.
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• Yitang Zhang, famoso pela conjectura dos primos gêmeos, estudou a conjectura jacobiana durante 7 anos em Purdue sob orientação de Tzuong-Tsieng Moh. Descobriu-se que uma etapa central de sua tese dependia de um corolário incorreto de Moh; Moh se recusou a escrever cartas de recomendação, e Zhang não conseguiu obter cargos de ensino ou pesquisa, acabando por trabalhar durante anos no Subway.
  Fico imaginando como teria sido se houvesse ChatGPT quando ele começou a pesquisa, em 1986. Hoje virou uma história de sucesso comovente, mas desperta sentimentos complexos, como no verso “a vida de Yu Xin foi profundamente desolada, mas seus poemas e rapsódias na velhice abalaram Jiangguan”.

  • Durante uma defesa de doutorado em matemática, um professor da banca encontrou uma falha na prova. Depois que o aluno entendeu e perguntou “e agora?”, o professor da banca apenas deu de ombros.
  • Pode-se dizer que é comovente porque ele mais tarde teve sucesso na conjectura dos primos gêmeos, mas estou cansado desse tipo de história na academia. Há política e gestão de reputação demais, e Zhang não deveria ter passado por esse sofrimento.
    Ao ampliar minha pesquisa para a matemática, fiquei surpreso ao ver que muitas proposições na literatura são falsas e se espalharam amplamente até na literatura aplicada. Mesmo quando se aponta o problema, muitas vezes a reação é defesa e negação, como na anedota de Zhang. LLMs são úteis para provas, mas também erram bastante; são como mais uma pessoa sugerindo direções de exploração a partir de outra intuição, então acho que em 1986 o resultado teria sido o mesmo.
  • O sentido do poema traduzido pelo ChatGPT é algo como: “A vida de Yu Xin foi completamente solitária, mas seus poemas e rapsódias na velhice abalaram rios e passagens”.

• Em matemática, contraexemplos são muito importantes para refinar definições e tornar provas mais afiadas. Recomendo o livro de 1976 de Imre Lakatos, 《Proofs and Refutations》, e há também muitos livros dedicados apenas a contraexemplos em topologia, teoria da probabilidade, análise etc.
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Encontrar um contraexemplo permite passar para outro problema sem desperdiçar tempo tentando provar uma proposição falsa; portanto, ao menos na matemática, ajuda a usar o tempo da humanidade de forma mais produtiva.

  • A refutação por contraexemplo é eficaz, mas no fim não é plenamente satisfatória. Ela dá uma resposta, mas não ajuda a entender por que a matemática funciona daquele jeito nem conduz a novas perguntas.
    Enquanto humanos julgarem o que é uma prova elegante e perspicaz, ainda haverá trabalho para matemáticos humanos.
  • Contraexemplos também são úteis para refinar o enunciado de um teorema. Em pesquisa em ciência da computação teórica, é comum tentar provar um teorema que gostaríamos que fosse verdadeiro, encontrar um contraexemplo, corrigir o enunciado e seguir em frente.
    Também ajuda o fato de muitos teoremas da ciência da computação lidarem com definições indutivas e coindutivas.
  • Especialmente se o contraexemplo tiver sido verificado formalmente, ele transforma quase instantaneamente anos de esforço conjectural em uma resposta definitiva.
  • Mas, no conjunto, não dá para afirmar que o tempo foi usado de forma mais produtiva. Seja provando ou refutando uma proposição, e quer ela acabe sendo verdadeira ou falsa, novos insights podem surgir no processo.

• Parece que a versão matemática de 《A Balada de John Henry》 também será escrita pela IA. Fico curioso para saber quem será o último campeão humano a apresentar uma prova “digna de entrar em THE BOOK” que nem mesmo as máquinas consigam superar.
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Essa é uma visão pouco saudável da matemática como competição, como a de torcedores de futebol. O mais valioso na matemática não são apenas provas bonitas, mas definições úteis, e criar boas definições e boas conjecturas a partir delas é um território que LLMs ainda não tentaram conquistar.
  • Ainda não é tão dramático, mas é possível que cheguemos a esse estágio em breve. Não há base para prever estruturalmente se as capacidades da IA avançarão de forma assintótica ou acelerada, e ambas as possibilidades permanecem abertas quanto a quais problemas serão resolvidos por novos métodos.
    Não entendemos o interior das capacidades da IA nem sua curva de crescimento, e sequer sabemos com precisão se ela está sendo deliberadamente exibida com desempenho reduzido. Pode ser um fenômeno emergente que resiste à medição, ou pode se tornar previsível como um relógio em alguns anos. Ninguém sabe; se alguém sabe, não está dizendo, e mesmo as pessoas mais barulhentas não sabem nada.

• Se isso acelerar significativamente os resultados relevantes de um doutorando, não há motivo para não investir US$ 2.400 por aluno por ano. No custo total, é quase troco

  • Alguns doutorandos se veem como seres éticos, não como “máquinas que produzem resultados relevantes”. Todo mundo sabe que até LLMs úteis são difíceis de justificar por causa dos dados de treinamento apropriados sem autorização e do enorme impacto ambiental
  • A bolsa de custo de vida de um doutorado do EPSRC é de cerca de £20.000, então isso corresponde a cerca de 10% do custo anual. Para o estudante individual, é um peso grande

• Eu gostaria que, na época da universidade, existissem formalizações em Lean feitas por LLMs. A matemática dos slides das aulas tinha muitos erros, e alguns professores recusavam pedidos de esclarecimento dizendo que “a prova está nos slides”, ao mesmo tempo em que relutavam em admitir os erros
  A prova em Lean em si muitas vezes não é adequada para entendimento, mas espero que, a partir dela, seja possível gerar argumentos mais fáceis de entender por humanos

  • Acho difícil concordar com a primeira afirmação. A curva de aprendizado é íngreme, mas formalizações em Lean·Agda·Rocq bem escritas são excelentes para entender uma prova. Uma boa formalização mostra estruturalmente a visão geral e os argumentos centrais e, diferentemente de uma prova em papel, permite verificar os detalhes de todos os passos até a profundidade desejada
    O repositório TypeTopology Agda de Martín Escardó é um bom exemplo. Por outro lado, as formalizações geradas por LLMs hoje podem ser muito bagunçadas; mesmo que certifiquem verdades e contenham argumentos interessantes, é preciso bastante trabalho para refiná-las em uma forma que aumente a compreensão matemática. O tutorial interativo de Agda está em lets-play-agda.quasicoherent.io
  • A formalização também pode ser usada numa abordagem leibniziana para encerrar debates e eliminar completamente dúvidas

• Fico curioso se, para matemáticos, um contraexemplo é como um resultado inesperado nas ciências físicas — algo incômodo no momento, mas que pode ser tremendamente importante por revelar a imprecisão de um modelo — ou se é como um relatório de bug em programação, um detalhe pequeno e irritante

  • Contraexemplos esclarecem o papel das condições. É muito útil ter o contraexemplo mais simples e memorável que mostre o que falha quando cada condição de uma prova é violada
    Matemáticos tendem a carregar na cabeça um zoológico de contraexemplos. Ao reconstruir um teorema, também podem se lembrar de contraexemplos incisivos e memoráveis e restringir o domínio e as condições de modo a excluí-los
  • Há livros didáticos, como 《Counterexamples in Topology》 e 《Counterexamples in Analysis》, que ensinam as sutilezas de uma área por meio de contraexemplos. Eles são populares porque é mais fácil aprender os detalhes a partir de exemplos patológicos e degenerados do que aprendendo apenas os objetos normais pretendidos

• Grande parte dessa matemática é difícil de entender, mas parece tratar principalmente de demonstrações de teoremas. Se a matemática com IA continuar acelerando, fico curioso se no futuro ela descobrirá até nova matemática que será aplicada à engenharia ou à biomedicina, se estamos às vésperas de uma grande ruptura para a humanidade, ou se ficará apenas em provar coisas já conhecidas

  • Há essa possibilidade. Compressed sensing pode ser visto como um exemplo de nova matemática aplicada à biomedicina; ele pode reduzir muito o tempo de exames de MRI, melhorando a experiência do paciente e permitindo que mais pacientes façam o exame
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Mesmo que haja aplicações em engenharia e biomedicina, provavelmente será algo de longo prazo; mas o desenvolvimento de novos métodos matemáticos pode se tornar importante mais cedo para a pesquisa em física fundamental. Muitas vezes, modelos melhoraram bastante quando surgiram ferramentas matemáticas que permitiram representar ou verificar modelos do universo
  • Mesmo que seja possível, levará muito tempo. Na maioria das áreas aplicadas, ainda estamos começando a usar adequadamente até matemática de centenas de anos atrás

• Algum dia, matemáticos podem ficar soterrados em provas a revisar, e proposições falsas aceitas com excesso de confiança podem entrar na comunidade matemática. Talvez os matemáticos do futuro, como engenheiros de software que usam IA, acabem examinando milhares de linhas de provas geradas por IA para encontrar erros sutis

  • Esse momento já chegou há muito tempo. A literatura hoje é enorme e cheia de provas incorretas, e entre os resultados publicados há certamente uma quantidade desconhecida, mas definitivamente não zero, de resultados falsos