Lean e a autoformalização: IA formaliza provas matemáticas em escala

A discussão sobre o Lean, um provador de teoremas usado na formalização de provas matemáticas, destaca como sistemas desse tipo verificam resultados no nível das regras lógicas e das bases da matemática. O texto lembra que o mathlib, biblioteca do ecossistema Lean, reúne quase 300 mil teoremas, mais de 100 mil definições e cerca de 2,5 milhões de linhas de código, com participação de mais de 700 colaboradores.

O avanço mais recente apontado é a autoformalização: a ideia de que sistemas de IA podem ler textos matemáticos e produzir provas formais no Lean (ou em outros assistentes). Em 2025 e 2026, projetos citados vão de uma quasi-autoformalização do teorema dos números primos até a autoformalização de grandes partes de livros, incluindo o Teorema de Fermat anunciado pela Anthropic em 4 de setembro e a formalização do problema de blowup de Navier-Stokes com forcing, associada à OpenAI em 8 de setembro.