Terence Tao escreve para matemáticos sobre a confiabilidade do Lean e o papel da IA

Em 9 de outubro de 2026, Terence Tao publicou em seu blog o post «What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI». O público-alvo está claro pelo título: matemáticos profissionais que estão de olho na verificação formal e em sistemas de IA que escrevem demonstrações. No Hacker News, a publicação somou 53 pontos e 7 comentários. Ao nosso feed chegou apenas o link, sem o texto, por isso não resumimos os argumentos do autor. Abaixo, analisamos o contexto em que esse tipo de post aparece e por que ele importa.

Por que a questão da confiabilidade virou um problema prático

O Lean começou como um projeto de Leonardo de Moura na Microsoft Research, em 2013. Hoje é uma ferramenta de trabalho para grandes projetos colaborativos. O próprio Tao participou, no fim de 2023, da formalização da conjectura PFR, que levou cerca de três semanas. Em 2024, ele coordenou o Equational Theories Project, que precisava determinar 22 028 942 implicações entre 4694 identidades em magmas. Sem automação e verificação formal, nem as pessoas nem os revisores dariam conta de um volume desses.

Em paralelo, os modelos de linguagem passaram a trabalhar com o Lean. Em julho de 2024, o AlphaProof, do Google DeepMind, resolveu quatro dos seis problemas da IMO e marcou 28 pontos de 42. As demonstrações saíam em Lean. Desde então, a pergunta «dá para confiar no que sai dessa cadeia?» deixou de ser filosofia da matemática e passou a fazer parte do trabalho cotidiano.

Onde passa a fronteira da confiança

O Lean tem um pequeno núcleo que verifica cada termo da demonstração. Táticas, automação e código gerado por modelos ficam fora do núcleo. Se errarem, o núcleo simplesmente rejeita o resultado. É isso que torna a combinação com a IA atraente: uma alucinação na demonstração é detectada de forma mecânica.

Restam pontos em que a confiança precisa ser avaliada separadamente:

• Formulação do teorema. O núcleo confirma que o enunciado escrito foi provado. Se ele coincide com o que se pretendia, quem decide é o humano.
• Definições. Uma definição imprecisa na biblioteca ou no arquivo esvazia de conteúdo o teorema provado.
• Axiomas. O Lean se apoia em `propext`, `Classical.choice` e `Quot.sound`. O comando `#print axioms` mostra quais foram usados.
• `sorry`. É um marcador no lugar da demonstração. Um arquivo com ele compila, mas o teorema não está provado.
• `native_decide`. A tática inclui o compilador na base de confiança, e `Lean.ofReduceBool` aparece na lista de axiomas.
• Implementação do núcleo. Existem verificadores independentes, como o lean4checker e reverificações de terceiros, que reduzem o risco de erro no próprio núcleo.

O que a IA muda

Antes dos modelos, o principal limite era o trabalho do formalizador. O modelo tira parte dessa carga, porque gera centenas de candidatas a demonstração. A verificação pelo núcleo continua barata. Em compensação, ganha destaque a segunda tarefa: garantir que o enunciado formal realmente diz o que o autor tinha em mente. O núcleo não faz esse trabalho, e um modelo que ajusta a demonstração à formulação pode encontrar brechas na própria formulação. Um exemplo típico: o enunciado se cumpre de forma trivial por causa de um conjunto vazio ou de uma divisão por zero mal definida.

Disso decorre uma conclusão prática: a auditoria se desloca dos passos da demonstração para as condições do problema. Para os matemáticos, é mais uma mudança de habilidade do que uma perda de controle.

Como trabalhar com isso

Se você pretende usar o Lean ou um assistente de IA em pesquisa, vale seguir uma ordem curta de ações:

• Escreva ou releia você mesmo as formulações dos teoremas, mesmo que a demonstração tenha sido gerada por um modelo.
• Antes de publicar, execute `#print axioms` e procure por `sorry`.
• Verifique se as definições usadas do Mathlib correspondem ao seu entendimento. Em casos não padronizados, escreva contraexemplos e lemas de verificação.
• Para resultados críticos, passe o arquivo por uma ferramenta de verificação independente.
• Leia o post original de Tao. Aqui demos o contexto, mas os argumentos e as recomendações dele são melhor buscados na fonte primária.