Lean Programming Language

If you want the full website experience, enable JS

The Proof in the Code by Kevin Hartnett FROM Quanta Books | Pre-order now, available June 9

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 > 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 > 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.

FEATURED PROJECTS<br>Lean in Action

Showcasing Real-World Applications

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, and verified AI across our systems.

Byron Cook

VP and Distinguished Scientist, AWS

At Google DeepMind, we used Lean to build AlphaProof, a new reinforcement-learning based system for formal math reasoning. Lean’s extensibility and verification capabilities were key in enabling the development of AlphaProof.

Pushmeet Kohli

VP, Science and Strategic Initiatives, Google DeepMind

Mathematical Superintelligence (MSI) with Lean will play a critical role in any industry where safety is paramount, including aerospace, automotive, and medical technology. In addition, we look forward to providing early access to our technology to students and researchers to accelerate advancement in mathematics, science, and engineering.

Tudor Achim

Co-Founder and CEO, Harmonic

Lean is the core verification technology behind Cedar, the open-source authorization language that powers cloud services like Amazon Verified Permissions and AWS Verified Access. Our team rigorously formalizes and verifies core components of Cedar using Lean’s proof assistant, and we leverage Lean’s lightning-fast runtime to continuously test our production Rust code against the Lean formalization. Lean’s efficiency, extensive libraries, and vibrant community enable us to develop and maintain Cedar at scale, while...