Lean Programming Language

If you want the full website experience, enable JS

The Proof in the Code by Kevin Hartnett FROM Quanta Books | available now

Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code

InstallLearn

Powerful automation

Mathematics

-- 'Grind' efficiently manages complex pattern matching and<br>-- case analysis beyond standard tactics.

example (x : Nat) : 0 match x with<br>| 0 => 1<br>| n+1 => x + n := by<br>grind

-- Automatically solves systems of linear inequalities.

example (x y : Int) :<br>27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45<br>→ -10 ≤ 7*x - 9*y → 7*x - 9*y _»-402">> 4 := by<br>grind

/-- A prime is a number larger than 1 with no trivial divisors -/<br>def IsPrime (n : Nat) := 1 n ∧ ∀ k, 1 k → k n → ¬ k ∣ n

/-- Every number larger than 1 has a prime factor -/<br>theorem exists_prime_factor :<br>∀ n, 1 n → ∃ k, IsPrime k ∧ k ∣ n := by<br>intro n h1<br>-- Either `n` is prime...<br>by_cases hprime : IsPrime n<br>· grind [Nat.dvd_refl]<br>-- ... or it has a non-trivial divisor with a prime factor<br>· obtain ⟨k, _⟩ : ∃ k, 1 k ∧ k n ∧ k ∣ n := by<br>simp_all [IsPrime]<br>obtain ⟨p, _, _⟩ := exists_prime_factor k (by grind)<br>grind [Nat.dvd_trans]

/-- The factorial, defined recursively, with custom notation -/<br>def factorial : Nat → Nat<br>| 0 => 1<br>| n+1 => (n + 1) * factorial n<br>notation:10000 n "!" => factorial n

/-- The factorial is always positive -/<br>theorem factorial_pos : ∀ n, 0 n ! := by<br>intro n; induction n grind [factorial]

/-- ... and divided by its constituent factors -/<br>theorem dvd_factorial : ∀ n, ∀ k ≤ n, 0 k → k ∣ n ! := by<br>intro n; induction n<br>grind [Nat.dvd_mul_right, Nat.dvd_mul_left_of_dvd, factorial]

/--<br>We show that we find arbitrary large (and thus infinitely<br>many) prime numbers, by picking an arbitrary number `n`<br>and showing that `n! + 1` has a prime factor larger than `n`.<br>-/<br>theorem InfinitudeOfPrimes : ∀ n, ∃ p _»-1833">> n, IsPrime p := by<br>intro n<br>have : 1 n ! + 1 := by grind [factorial_pos]<br>obtain ⟨p, hp, _⟩ := exists_prime_factor (n ! + 1) this<br>suffices ¬p ≤ n by grind<br>intro (_ : p ≤ n)<br>have : 1 p := hp.1<br>have : p ∣ n ! := dvd_factorial n p ‹p ≤ n› (by grind)<br>have := Nat.dvd_sub ‹p ∣ n ! + 1› ‹p ∣ n !›<br>grind [Nat.add_sub_cancel_left, Nat.dvd_one]

Grind is a powerful tool that can help you prove theorems quickly and efficiently.

A definition of prime numbers and a proof that there are infinitely many prime numbers.

Lean's minimal trusted kernel guarantees absolute correctness in mathematical proof, software and hardware verification.

From elementary concepts to cutting-edge research, Lean's expressive language and extensive built-in tools let users focus on the big picture rather than routine details.

Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.

Get Started with Lean

Lean lets you write precise, verifiable code and formal proofs. Whether you are new or experienced, now is a great time to start.

InstallLearn

FEATURED PROJECTS<br>Lean in Action

Showcasing Real-World Applications

PROGRESS<br>Growth and Impact

Tracking Lean's reach across math, research, and industry

About Lean

Learn more about Lean from its origins to its growing global impact

READ MORE →

Roadmap

The Lean FRO's annual technical priorities and planned deliverables for Lean

EXPLORE THE ROADMAP →

JULY 2026

Microsoft Research reports on how Lean, via the Aeneas toolchain, formally verifies production cryptographic algorithms in SymCrypt; New Scientist reports on AI use supporting the Lean formalization of Fermat's Last Theorem

JUNE, 2026

Quanta Books publishes The Proof in the Code, "the definitive account of the birth and rise of Lean"; Fortune magazine announces Axiom's EconLib, formalizing economic theory in Lean; StatLib, a library for mathematical statistics, is launched

MAY, 2026

Google DeepMind announces AlphaProof Nexus and autonomous proofs of 9 Erdős problems; SAIR convenes the Science x AI Summit in Palo Alto, foregrounding Lean and AI-assisted proof discovery; NASA holds its Formal Methods Symposium with keynotes on Lean, CSLib and Aristotle; TorchLean is released, bridging PyTorch and Lean

READ MORE →

Lean enables large-scale collaboration by allowing mathematicians to break down complex proofs into smaller, verifiable components. This formalization process ensures the correctness of proofs and facilitates contributions from a broader community. With Lean, we are beginning to see how AI can accelerate the formalization of mathematics, opening up new possibilities for research.

Terence Tao

Mathematician, UCLA

Lean has become a key enabler in scaling automated reasoning at Amazon. Its capacity to verify complex systems involving advanced mathematical concepts has transformed how we tackle problems once thought too complex or impractical. Lean is an indispensable tool in modern, large-scale software engineering, helping ensure soundness, correctness,...