Trustworthy
Lean’s minimal trusted kernel guarantees absolute correctness in mathematical proof, software and hardware verification.
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code
Powerful automation
Mathematics
-- 'Grind' efficiently manages complex pattern matching and
-- case analysis beyond standard tactics.
example (x : Nat) : 0 < match x with
| 0 => 1
| n+1 => x + n := by
grind
-- Automatically solves systems of linear inequalities.
example (x y : Int) :
27 ≤ 11*x + 13*y → 11*x + 13*y ≤ 45
→ -10 ≤ 7*x - 9*y → 7*x - 9*y > 4 := by
grind/-- A prime is a number larger than 1 with no trivial divisors -/
def IsPrime (n : Nat) := 1 < n ∧ ∀ k, 1 < k → k < n → ¬ k ∣ n
/-- Every number larger than 1 has a prime factor -/
theorem exists_prime_factor :
∀ n, 1 < n → ∃ k, IsPrime k ∧ k ∣ n := by
intro n h1
-- Either `n` is prime...
by_cases hprime : IsPrime n
· grind [Nat.dvd_refl]
-- ... or it has a non-trivial divisor with a prime factor
· obtain ⟨k, _⟩ : ∃ k, 1 < k ∧ k < n ∧ k ∣ n := by
simp_all [IsPrime]
obtain ⟨p, _, _⟩ := exists_prime_factor k (by grind)
grind [Nat.dvd_trans]
/-- The factorial, defined recursively, with custom notation -/
def factorial : Nat → Nat
| 0 => 1
| n+1 => (n + 1) * factorial n
notation:10000 n "!" => factorial n
/-- The factorial is always positive -/
theorem factorial_pos : ∀ n, 0 < n ! := by
intro n; induction n <;>
grind [factorial, Nat.mul_pos_iff_of_pos_left]
/-- ... and divided by its constituent factors -/
theorem dvd_factorial : ∀ n, ∀ k ≤ n, 0 < k → k ∣ n ! := by
intro n; induction n <;>
grind [Nat.dvd_mul_right, Nat.dvd_mul_left_of_dvd, factorial]
/--
We show that we find arbitrary large (and thus infinitely
many) prime numbers, by picking an arbitrary number `n`
and showing that `n! + 1` has a prime factor larger than `n`.
-/
theorem InfinitudeOfPrimes : ∀ n, ∃ p > n, IsPrime p := by
intro n
have : 1 < n ! + 1 := by grind [factorial_pos]
obtain ⟨p, hp, _⟩ := exists_prime_factor (n ! + 1) this
suffices ¬p ≤ n by grind
intro (_ : p ≤ n)
have : 1 < p := hp.1
have : p ∣ n ! := dvd_factorial n p ‹p ≤ n› (by grind)
have := Nat.dvd_sub ‹p ∣ n ! + 1› ‹p ∣ n !›
grind [Nat.add_sub_cancel_left, Nat.dvd_one]
Powerful
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.
Extensible
Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.
FEATURED PROJECTS
Lean in Action
Showcasing Real-World Applications
Mathlib
Mathlib is Lean's comprehensive mathematical library containing over a million lines of formalized mathematics spanning algebra, analysis, topology, probability, and computer science. This community-driven resource enables mathematicians to tackle frontier research problems and engineers to build verified systems by providing a rigorously verified foundation of mathematical knowledge that eliminates duplication of effort.
Read More
Aeneas
Aeneas takes a novel approach to Rust verification. Unlike other verification approaches that must reason about memory directly, Aeneas leverages Rust's rich type system to eliminate memory reasoning entirely for many Rust programs.
Read More
Fermat's Last Theorem
The Fermat's Last Theorem project is formalizing one of mathematics' most complex proofs in Lean, demonstrating the theorem prover's capacity to handle frontier research mathematics. This ambitious work is creating formalized definitions for advanced number-theoretic objects, enabling mathematicians to build machine-verified proofs of cutting-edge results while establishing Lean as a powerful platform for mathematical collaboration.
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.
"
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.
"
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.
"
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.
"
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 ensuring the key correctness and security properties that our users depend on.
SUPPORTERS
Sponsors and Partners
With grateful acknowledgment of our contributing organizations
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.