Storia
Lean è stato sviluppato principalmente dall'informatico brasiliano Leonardo de Moura, prima durante il suo impiego presso Microsoft Research e successivamente presso Amazon Web Services, con importanti contributi da parte di altri coautori e collaboratori nel corso della sua storia.
Lanciato nel 2013, nelle sue prime versioni, note in seguito come Lean 1 e Lean 2, il linguaggio era sperimentale e comprendeva funzionalità poi abbandonate, come il supporto a fondamenti basati sulla teoria dei tipi omotopica.
Lean 3 (pubblicato per la prima volta il 20 gennaio 2017) è stata la prima versione ragionevolmente stabile di Lean. Era implementato principalmente in C++, con alcune funzionalità scritte in Lean stesso. Dopo la versione 3.4.2 lo sviluppo ufficiale di Lean 3 è terminato per concentrarsi su Lean 4; nel periodo di transizione alcuni membri della comunità hanno sviluppato e pubblicato versioni non ufficiali fino alla 3.51.1.
Nel 2021 è stato pubblicato Lean 4, una reimplementazione del dimostratore in grado di generare codice C che viene poi compilato, consentendo lo sviluppo di automazioni efficienti e specifiche per dominio. Lean 4 introduce inoltre un sistema di macro igieniche e procedure migliorate di sintesi delle classi di tipi e di gestione della memoria rispetto alla versione precedente. Un altro vantaggio rispetto a Lean 3 è la possibilità di modificare il frontend e altre parti chiave del sistema senza intervenire sul codice C++, poiché sono ora interamente implementate in Lean e possono essere ridefinite dall'utente secondo necessità.
Lean 4 non è retrocompatibile con Lean 3. Utilizza la versione C++17 del C++.
Nel 2023 è stata costituita la Lean FRO (Focused Research Organization), con l'obiettivo di migliorare la scalabilità e l'usabilità del linguaggio e di implementare l'automazione delle dimostrazioni.
Nel 2025 il Programming Languages Software Award dello SIGPLAN dell'ACM è stato assegnato a Gabriel Ebner, Soonho Kong, Leo de Moura e Sebastian Ullrich per Lean, con una motivazione che ne sottolinea il notevole impatto su matematica, verifica di hardware e software e intelligenza artificiale.
Nel 2026 la libreria mathlib ha ricevuto il premio Demailly per la scienza aperta.
Caratteristiche
Lean offre numerose funzionalità utili per la programmazione funzionale e la dimostrazione di teoremi, tra cui tipi dipendenti, classi di tipi, multithreading, un linguaggio di tattiche espressivo e un sistema di moduli.
Librerie
La libreria standard ufficiale di Lean si chiama Std e contiene strutture dati e funzioni di uso comune nella programmazione, come mappe ad albero, tabelle hash, funzioni per data e ora e primitive per la concorrenza. La libreria standard è affiancata da batteries, mantenuta dalla comunità, che implementa ulteriori strutture dati utilizzabili sia nella ricerca matematica sia nello sviluppo software più tradizionale.
Nel 2017 è iniziato lo sviluppo di mathlib, una libreria per Lean mantenuta dalla comunità con l'obiettivo di digitalizzare quanta più matematica pura possibile in un'unica grande libreria coerente, fino alla matematica di livello di ricerca. A maggio 2025 mathlib conteneva la formalizzazione in Lean di oltre 210 000 teoremi e 100 000 definizioni.
Tra le altre librerie figurano CSLib, dedicata all'informatica teorica, SciLean, per il calcolo scientifico in Lean, e PhysLib, il cui obiettivo è digitalizzare la fisica in Lean.
Integrazione con gli editor
Lean si integra con:
L'interfacciamento avviene tramite un'estensione client e un server basato sul Language Server Protocol. In questi editor i simboli Unicode possono essere digitati con sequenze simili a quelle di LaTeX, ad esempio \times per «×».
Esempi (Lean 4)
I numeri naturali possono essere definiti come tipo induttivo. Questa definizione si basa sugli assiomi di Peano e afferma che ogni numero naturale è o lo zero o il successore di un altro numero naturale.
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
L'addizione tra numeri naturali può essere definita ricorsivamente mediante pattern matching.
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)
Segue una semplice dimostrazione in modalità tattica di 
per due proposizioni 
e 
(dove 
indica la congiunzione e 
l'implicazione):
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
intro h -- si assume p ∧ q con dimostrazione h; l'obiettivo è q ∧ p
apply And.intro -- l'obiettivo si divide in due sotto-obiettivi: q e p
· exact h.right -- il primo sotto-obiettivo è esattamente la parte destra di h : p ∧ q
· exact h.left -- il secondo sotto-obiettivo è esattamente la parte sinistra di h : p ∧ q
La stessa dimostrazione in modalità termine:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
fun ⟨hp, hq⟩ => ⟨hq, hp⟩
Il teorema può essere dimostrato anche con la tattica grind, che sfrutta tecniche proprie dei risolutori SMT per costruire automaticamente le dimostrazioni:
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
grind
Utilizzi
Matematica
Lean ha attirato l'attenzione di matematici come Thomas Hales, Kevin Buzzard, Terence Tao e Heather Macbeth. Hales lo utilizza per il suo progetto Formal Abstracts, mentre Buzzard lo impiega per lo Xena project. Uno degli obiettivi dello Xena project è riscrivere in Lean ogni teorema e ogni dimostrazione del corso di laurea triennale in matematica dell'Imperial College London. Tao ha pubblicato un complemento in Lean al suo manuale di analisi reale Analysis I, costituito dalla formalizzazione di sezioni selezionate del testo. Macbeth usa Lean per insegnare agli studenti i fondamenti della dimostrazione matematica con un riscontro immediato.
Nel 2021 un gruppo di ricercatori ha utilizzato Lean per verificare la correttezza di una dimostrazione di Peter Scholze nell'ambito della matematica condensata. Il progetto ha suscitato interesse per aver formalizzato un risultato all'avanguardia della ricerca matematica. Nel 2023 Terence Tao ha usato Lean per formalizzare la dimostrazione della congettura polinomiale di Freiman-Ruzsa (PFR), un risultato pubblicato nello stesso anno da Tao e dai suoi collaboratori (vedi teorema di Freiman). Nel 2026 i problemi di Erdős numero 728, 347 e 369 sono stati risolti con l'ausilio dell'intelligenza artificiale e verificati formalmente con Lean.
Fisica
Physlib ambisce a diventare la libreria di riferimento per la fisica in Lean, sul modello di Mathlib per la matematica, e punta a raccogliere in modo completo definizioni, teoremi e calcoli fondamentali della fisica.
Kevin Buzzard dell'Imperial College London afferma che la formalizzazione sta avendo un forte impatto sulla matematica e che non vi è motivo per cui la fisica teorica non possa essere trattata allo stesso modo:
(inglese)
«Ideally, we need a million lines of physics, and that might be hard work to get. If the machines aren't pretty good at doing physics initially, then there'll be manual work at the beginning, and then eventually the machines will hopefully take over»
(italiano)
«Idealmente ci serve un milione di righe di fisica, e potrebbe essere un lavoro difficile da ottenere. Se all'inizio le macchine non saranno molto brave a fare fisica, ci sarà del lavoro manuale nella fase iniziale, e poi, si spera, le macchine prenderanno il sopravvento.»
Nel 2025 Joseph Tooby-Smith ha utilizzato Lean per individuare un errore in un articolo pubblicato nel 2006 sulla stabilità del potenziale del modello a due doppietti di Higgs (2HDM).
Intelligenza artificiale
Nel 2022 OpenAI e Meta AI hanno sviluppato, in modo indipendente, modelli di intelligenza artificiale in grado di generare in Lean dimostrazioni di vari problemi di olimpiadi della matematica di livello liceale. Il modello di Meta AI è disponibile pubblicamente per l'uso con l'ambiente Lean.
Nel 2023 Vlad Tenev e Tudor Achim hanno fondato la startup Harmonic, che mira a ridurre le allucinazioni dell'intelligenza artificiale generando e verificando codice Lean.
Nel 2024 Google DeepMind ha creato AlphaProof, un sistema che dimostra enunciati matematici in Lean al livello di un medagliato d'argento alle Olimpiadi Internazionali della Matematica. Si è trattato del primo sistema di intelligenza artificiale a ottenere una prestazione da medaglia sui problemi di un'olimpiade della matematica.
Nell'aprile 2025 DeepSeek ha presentato DeepSeek-Prover-V2, un modello di intelligenza artificiale progettato per la dimostrazione di teoremi in Lean 4 e basato su DeepSeek-V3.
Nel 2026 alcune intelligenze artificiali progettate per individuare bug nel software sono state applicate a Lean, scoprendo diverse falle che sono state poi corrette. Forse in relazione a questo lavoro, è stata annunciata una presunta confutazione della congettura di Collatz verificata in Lean; si è però presto scoperto che la dimostrazione sfruttava un bug di Lean e, una volta corretto il bug, è risultata non valida.
Nel settembre 2026 Anthropic ha reso noto che alcuni agenti basati su un modello di ricerca interno, paragonabile a Claude Fable 5.1, avevano prodotto in undici giorni una formalizzazione completa e verificata automaticamente dell'ultimo teorema di Fermat in Lean 4. La dimostrazione seguiva l'esposizione del 1995 di Darmon, Diamond e Taylor della dimostrazione di Wiles, comprendeva circa 13 milioni di righe di codice Lean e circa 30 000 teoremi intermedi, e si basava unicamente sui tre assiomi standard di Lean; gli agenti si coordinavano tramite Prove2Me, una piattaforma per la formalizzazione collaborativa sviluppata dal ricercatore di Anthropic Tianyi Peng insieme a collaboratori della Columbia University. Kevin Buzzard, che guida un distinto progetto dell'Imperial College London per formalizzare il teorema in Lean, ha compilato e controllato il codice confermando il risultato, pur osservando che dal punto di vista matematico esso «non aggiunge nulla» alla dimostrazione di Wiles e che il codice non poteva essere integrato in Mathlib. Buzzard ha dichiarato che il progetto dell'Imperial College sarebbe proseguito.
