IA começa a resolver teoremas e a escrever provas formais em Lean

ChatGPT refuta a conjectura da distância unitária de Erdős

Em 20 de maio de 2026, o ChatGPT apresentou uma refutação da conjectura da distância unitária de Erdős, um problema em aberto na geometria discreta. A prova usa um teorema profundo de teoria dos números de Golod e Shafarevich, da década de 1960, para construir um contraexemplo. Matemáticos que tiveram acesso antecipado ao argumento confirmaram sua plausibilidade. Kevin Buzzard, autor do post e mantenedor da biblioteca Lean mathlib, questionou imediatamente se o resultado havia sido formalizado em Lean - a resposta inicial era não.

Formalização automática em tempo real

Em menos de uma semana, Mike Freedman, medalhista Fields e Chief Science Officer da Logical Intelligence (empresa cofundada por Yann LeCun), informou que o sistema da empresa havia autoformalizado o artigo inteiro em Lean. O resultado formalizava a implicação do teorema de Golod-Shafarevich no contraexemplo de Erdős. O desafio restante era o próprio teorema de Golod-Shafarevich, cuja prova informal ocupa mais de 100 páginas e depende de teoria de corpos de classes global - uma área cuja formalização em Lean parecia inviável até pouco tempo antes.

Sol gera 1,2 milhão de linhas de Lean em três semanas

Em 26 de junho de 2026, Boris Alexeev, pesquisador da OpenAI, anunciou no Lean Zulip que havia guiado o modelo Sol para uma formalização completa do contraexemplo de Erdős, sem assumir nada além dos axiomas da matemática. O código, tornado público, continha provas de teoremas não triviais em cohomologia de corpos numéricos e teoria de corpos de classes global. O Sol gerou 1,2 milhão de linhas de código Lean em três semanas - a mathlib inteira, com 2,3 milhões de linhas, levou nove anos para ser escrita por humanos. Buzzard executou o código em sandbox e confirmou que as provas compilavam corretamente.

Contraexemplo à pergunta de Grothendieck e à conjectura Jacobiana

Durante o workshop Formalizing Fermat (6 a 10 de julho de 2026), Akhil Mathew, professor da Universidade de Chicago, pediu ao Sol que investigasse uma pergunta de Grothendieck de 1966: se todo esquema de grupo finito livre de ordem n é aniquilado por n. Em 11 de julho, o Sol encontrou um contraexemplo - um esquema de grupo de ordem 4 não aniquilado por 4. O modelo Fable autoformalizou o resultado em 1.076 linhas de Lean, e Buzzard verificou a prova em menos de 5 minutos. Pouco depois, Levent Alpöge anunciou que o Fable havia encontrado um contraexemplo à conjectura Jacobiana, um problema famoso em geometria algébrica aberto há 100 anos. O resultado foi formalizado manualmente por Paul Lezeau e submetido ao repositório Formal Conjectures da DeepMind.

Impacto na produtividade e reações da comunidade

Andrew Yang, doutorando de Buzzard, usou Sol e Fable para escrever 250 mil linhas de Lean em cerca de duas semanas, completando a formalização de um teorema de levantamento de modularidade crucial para o trabalho sobre o Último Teorema de Fermat. Buzzard afirmou que qualquer doutorando que não pagasse US$ 200 mensais por acesso a esses modelos estava "louco". Harvard já oferece acesso gratuito ao Fable para todos os doutorandos, pós-docs e professores. As reações na comunidade variam: alguns veem os resultados como evidência de que os problemas não eram tão difíceis, outros expressam preocupação com a dessqualificação da pesquisa matemática e com o papel futuro dos matemáticos quando provas formais são geradas por máquinas.