Lean é um assistente de provas e uma linguagem de programação funcional. É baseado no cálculo de construções com tipos indutivos (especificamente, o Cálculo de Construções Indutivas), a teoria dos tipos fundamental desenvolvida com o provador de teoremas Coq, que foi renomeado para Rocq em 2024. É um projeto de software livre e de código aberto hospedado no GitHub. O desenvolvimento é atualmente apoiado pela Lean Focused Research Organization (FRO), uma organização sem fins lucrativos.
História O Lean foi desenvolvido primariamente pelo cientista da computação brasileiro Leonardo de Moura enquanto trabalhava na Microsoft Research e, posteriormente, na Amazon Web Services, contando com contribuições significativas de outros coautores e colaboradores ao longo de sua história.
Lançadas em 2013, as versões iniciais da linguagem, mais tarde conhecidas como Lean 1 e 2, eram experimentais e continham recursos como suporte a fundamentos baseados na teoria dos tipos homotópicos, que posteriormente foram abandonados.
O Lean 3 (lançado inicialmente em 20 de janeiro de 2017) foi a primeira versão moderadamente estável do Lean. Foi implementado principalmente em C++, com alguns recursos escritos no próprio Lean. Após a versão 3.4.2, o ciclo de vida do Lean 3 foi oficialmente encerrado, iniciando-se o desenvolvimento do Lean 4. Nesse período intermediário, membros da comunidade do Lean desenvolveram e lançaram versões não oficiais até a 3.51.1.
Em 2021, foi lançado o Lean 4, uma reimplementação do provador de teoremas Lean capaz de produzir código em C que é posteriormente compilado, viabilizando o desenvolvimento de automações específicas de domínio altamente eficientes. O Lean 4 também introduziu um sistema de macros higiênicas e aprimoramentos nos procedimentos de síntese de classe de tipos e de gerenciamento de memória em relação à versão anterior. Outro benefício em relação ao Lean 3 é a possibilidade de evitar a modificação de código em C++ para alterar o frontend e outros componentes centrais do sistema, visto que agora são implementados em Lean e estão disponíveis para serem sobrescritos pelo usuário final conforme a necessidade.
O Lean 4 não possui retrocompatibilidade com o Lean 3. Ele utiliza o padrão C++17 do C++.
Em 2023, foi formada a Lean FRO (Focused Research Organization), com a meta de aprimorar a escalabilidade e a usabilidade da linguagem, além de implementar automação de provas.
Em 2025, o Prêmio de Software de Linguagens de Programação da ACM SIGPLAN foi concedido a Gabriel Ebner, Soonho Kong, Leo de Moura e Sebastian Ullrich pelo Lean, citado pelo seu "impacto significativo na matemática, na verificação de hardware e software e na IA".
Em 2026, a biblioteca mathlib recebeu o Prêmio Demailly para ciência aberta.
Visão geral O Lean inclui diversos recursos úteis para programação funcional e demonstração de teoremas, como tipos dependentes, classes de tipos, multithreading, uma linguagem expressiva de táticas e um sistema de módulos.
Bibliotecas A biblioteca padrão oficial do Lean chama-se Std e contém estruturas de dados comuns e funções essenciais para programação, como mapas em árvore (tree maps), tabelas hash (hash maps), funções de data e hora e primitivas de concorrência. A biblioteca padrão é complementada pela batteries, mantida pela comunidade, que implementa estruturas de dados adicionais utilizáveis tanto em pesquisa matemática quanto no desenvolvimento convencional de software.
Em 2017, teve início um projeto mantido pela comunidade para desenvolver uma biblioteca do Lean chamada mathlib, com o objetivo de digitalizar o máximo possível da matemática pura em uma única biblioteca coesa, abrangendo até a matemática em nível de pesquisa. Até maio de 2025, a mathlib já havia formalizado mais de 210.000 teoremas e 100.000 definições em Lean.
Outras bibliotecas incluem a CSLib, voltada para a ciência da computação teórica, a SciLean, focada em computação científica em Lean, e a PhysLib, cujo objetivo é digitalizar a física com o auxílio do Lean.
Integração com editores O Lean integra-se com: Visual Studio Code Neovim Emacs
A comunicação é estabelecida por meio de uma extensão cliente e um servidor baseado no Language Server Protocol (LSP). Nesses editores, símbolos Unicode podem ser inseridos por meio de sequências no estilo LaTeX, como para "×".
Exemplos (Lean 4) Os números naturais podem ser definidos como um tipo indutivo. Esta definição fundamenta-se nos axiomas de Peano e postula que todo número natural é zero ou o sucessor de algum outro número natural: inductive Nat : Type | zero : Nat | succ : Nat → Nat
A adição de números naturais pode ser definida recursivamente, utilizando casamento de padrões: def Nat.add : Nat → Nat → Nat | n, Nat.zero => n -- n + 0 = n | n, Nat.succ m => Nat.succ (Nat.add n m) -- n + succ(m) = succ(n + m)
Abaixo apresenta-se uma demonstração simples de para duas proposições e (onde representa a conjunção lógica e a implicação material) no Lean utilizando o modo tático: theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by intro h -- assume p ∧ q com prova h; o objetivo é q ∧ p apply And.intro -- divide o objetivo em dois subobjetivos: q e p · exact h.right -- o primeiro subobjetivo é a parte direita de h : p ∧ q · exact h.left -- o segundo subobjetivo é a parte esquerda de h : p ∧ q
A mesma demonstração no modo de termos: theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := fun ⟨hp, hq⟩ => ⟨hq, hp⟩
O teorema também pode ser provado utilizando a tática `grind`, que emprega técnicas de resolvedores SMT para derivar demonstrações automaticamente: theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by grind
Aplicações
Matemática O Lean atraiu a atenção de matemáticos como Thomas Hales, Kevin Buzzard, Terence Tao, e Heather Macbeth. Hales o utiliza em seu projeto Formal Abstracts. Buzzard o emprega no projeto Xena. Um dos objetivos do projeto Xena é reescrever em Lean todos os teoremas e provas do currículo de graduação em matemática do Imperial College London. Tao disponibilizou um guia complementar em Lean para o seu livro-texto de análise real Analysis I, composto pela formalização de seções selecionadas da obra. Macbeth utiliza o Lean para instruir estudantes nos fundamentos da demonstração matemática com retorno imediato (feedback).
Formalizações notáveis
Em 2021, uma equipe de pesquisadores utilizou o Lean para verificar a exatidão de uma demonstração elaborada por Peter Scholze no campo da matemática condensada. O projeto obteve grande repercussão por formalizar um resultado na fronteira da pesquisa matemática. Em 2023, Terence Tao recorreu ao Lean para formalizar a prova da conjectura polinomial de Freiman-Ruzsa (PFR), resultado divulgado por Tao e coautores no mesmo ano. Em 2026, os problemas 728, 347, e 369 da lista de problemas de Erdős foram solucionados com suporte de inteligência artificial e verificados formalmente no Lean.
Física A Physlib busca consolidar-se como a biblioteca de referência para a física no Lean, exercendo papel equivalente ao da Mathlib para a matemática. Sua finalidade é ser um repositório abrangente com definições basilares, teoremas e cálculos da física. Kevin Buzzard, do Imperial College London, pontua que a formalização está gerando transformações profundas na matemática, e que não há razão para que a física teórica não receba o mesmo tratamento. “Idealmente, precisamos de um milhão de linhas de física, e isso pode dar bastante trabalho. Se as máquinas não forem muito boas em lidar com a física logo de início, haverá trabalho manual no começo, e eventualmente espera-se que as máquinas assumam o controle.”
Formalizações notáveis Em 2025, Joseph Tooby-Smith utilizou o Lean para identificar uma inconsistência em um artigo publicado em 2006 sobre a estabilidade do potencial no modelo de dois dubletos de Higgs (2HDM).
Inteligência artificial
Em 2022, a OpenAI e a Meta AI criaram independentemente modelos de IA para derivar demonstrações de vários problemas matemáticos de nível escolar/olímpico no Lean. O modelo da Meta AI foi liberado publicamente para uso conjugado ao ambiente do Lean.
Em 2023, Vlad Tenev e Tudor Achim cofundaram a startup Harmonic, voltada a mitigar alucinações em modelos de linguagem por meio da geração e validação de código em Lean.
Em 2024, a Google DeepMind apresentou o AlphaProof, sistema que demonstrou proposições matemáticas em Lean com desempenho correspondente ao de um medalhista de prata na Olimpíada Internacional de Matemática. Trata-se do primeiro sistema computacional de IA a conquistar nível de premiação na competição.
Em abril de 2025, a DeepSeek lançou o DeepSeek-Prover-V2, modelo concebido para demonstração automática de teoremas em Lean 4, estruturado a partir do DeepSeek-V3.
Em 2026, modelos de IA concebidos para encontrar falhas em software foram aplicados ao código do Lean, detectando brechas de consistência que foram prontamente solucionadas. Em paralelo a esse processo, uma suposta refutação da conjectura de Collatz chegou a ser anunciada como validada em Lean; contudo, verificou-se que a demonstração se apoiava em uma inconsistência no núcleo do provador. Corrigida a falha, a demonstração foi invalidada.
Em setembro de 2026, a Anthropic anunciou que agentes baseados em um modelo interno de pesquisa (comparável ao Claude Fable 5.1) completaram a formalização integral do Último Teorema de Fermat em Lean 4 no intervalo de onze dias. A demonstração seguiu a abordagem exposta em 1995 por Darmon, Diamond e Taylor sobre a prova de Wiles, compreendendo aproximadamente 13 milhões de linhas de código e cerca de 30.000 teoremas intermediários, apoiando-se estritamente nos três axiomas canônicos do Lean. A coordenação entre os agentes ocorreu por meio da plataforma Prove2Me, desenvolvida pelo pesquisador Tianyi Peng com colaboradores da Universidade Columbia. Kevin Buzzard, coordenador de iniciativa paralela no Imperial College London com o mesmo objetivo, compilou e atestou o resultado, ressalvando que ele "não adiciona novidades" teóricas à demonstração original de Wiles e que o código produzido não seria incorporado diretamente à Mathlib. Buzzard ressaltou que o projeto no Imperial College terá continuidade.
Ver também Tipo dependente Lista de assistentes de provas mimalloc Teoria dos tipos
Referências
Ligações externas
Comunidade Lean Lean FRO The Natural Number Game - tutorial interativo para o aprendizado de Lean Moogle.ai - ferramenta de busca semântica para teoremas na mathlib Categoria:Linguagens de programação funcionais Categoria:Software livre programado em C++