Lean (proof assistant)

Proof assistant and programming language

Lean

Paradigm| Functional programming, Imperative programming
Family| Proof assistant
Developer| Lean FRO
First appeared| 2013; 12 years ago (2013)
Stable release|

4.21.0[1]  / 30 June 2025; 28 days ago (30 June 2025)

Typing discipline| Static, strong, inferred
Implementation language| Lean, C++
OS| Cross-platform
License| Apache License 2.0
Website| lean-lang.org
Influenced by

Rocq (previously known as Coq)
Haskell

Lean is a proof assistant and a functional programming language.[2] It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. Development is currently supported by the non-profit Lean Focused Research Organization (FRO).

## History

[edit]

Lean was developed primarily by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history.

It was launched by Leonardo de Moura at Microsoft Research in 2013.[3] The initial versions of the language, later known as Lean 1 and 2, were experimental and contained features such as support for homotopy type theory – based foundations that were later dropped.

Lean 3 (first released Jan 20, 2017) was the first moderately stable version of Lean. It was implemented primarily in C++ with some features written in Lean itself. After version 3.4.2 Lean 3 was officially end-of-lifed while development of Lean 4 began. In this interim period members of the Lean community developed and released unofficial versions up to 3.51.1.

In 2021, Lean 4 was released, which was a reimplementation of the Lean theorem prover capable of producing C code which is then compiled, enabling the development of efficient domain-specific automation.[4] Lean 4 also contains a macro system and improved type class synthesis and memory management procedures over the previous version. Another benefit compared to Lean 3 is the ability to avoid touching C++ code in order to modify the frontend and other key parts of the core system, as they are now all implemented in Lean and available to the end user to be overridden as needed.[2]

Lean 4 is not backwards-compatible with Lean 3.[5]

In 2023, the Lean FRO was formed, with the goals of improving the language's scalability and usability, and implementing proof automation.[6]

In 2025, ACM SIGPLAN Programming Languages Software Award was awarded to Gabriel Ebner, Soonho Kong, Leo de Moura and Sebastian Ullrich for Lean, cited for its "significant impact on mathematics, hardware and software verification, and AI".[7]

## Overview

[edit]

### Libraries

[edit]

The official lean package includes a standard library batteries, which implements common data structures that may be used for both mathematical research and more conventional software development.[8]

In 2017, a community-maintained project to develop a Lean library mathlib began, with the goal to digitize as much of pure mathematics as possible in one large cohesive library, up to research level mathematics.[9][10] As of May 2025, mathlib had formalized over 210,000 theorems and 100,000 definitions in Lean.[11]

### Editors integration

[edit]

Lean integrates with:[12]

* Visual Studio Code
* Neovim
* Emacs

Interfacing is done via a client-extension and Language Server Protocol server.

It has native support for Unicode symbols, which can be typed using LaTeX-like sequences, such as "\times" for "×". Lean can also be compiled to JavaScript and accessed in a web browser and has extensive support for meta-programming.

## Examples (Lean 4)

[edit]

The natural numbers can be defined as an inductive type. This definition is based on the Peano axioms and states that every natural number is either zero or the successor of some other natural number.

inductive Nat : Type
| zero : Nat
| succ : Nat → Nat

Addition of natural numbers can be defined recursively, using 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)

This is a simple proof of  ( P ∧ Q ) ⟹ ( Q ∧ P ) {\displaystyle (P\wedge Q)\implies (Q\wedge P)} for two propositions P and Q (where  ∧ {\displaystyle \wedge } is the conjunction and  ⟹ {\displaystyle \implies } the implication) in Lean using tactic mode:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
intro h            -- assume p ∧ q with proof h, the goal is q ∧ p
apply And.intro    -- the goal is split into two subgoals, one is q and the other is p
· exact h.right    -- the first subgoal is exactly the right part of h : p ∧ q
· exact h.left     -- the second subgoal is exactly the left part of h : p ∧ q

This same proof in term mode:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
fun ⟨hp, hq⟩ => ⟨hq, hp⟩

## Usage

[edit]

### Mathematics

[edit]

See also: Proof assistant § Notable formalized proofs

Lean has received attention from mathematicians such as Thomas Hales,[13] Kevin Buzzard,[14] Terence Tao,[15] and Heather Macbeth.[16] Hales is using it for his project, Formal Abstracts.[17] Buzzard uses it for the Xena project.[18] One of the Xena Project's goals is to rewrite every theorem and proof in the undergraduate math curriculum of Imperial College London in Lean. Tao released a Lean companion to his Real analysis textbook Analysis I, consisting of a formalization of selected sections of the mathematical text.[19] Macbeth is using Lean to teach students the fundamentals of mathematical proof with instant feedback.[20]

#### Noteworthy formalizations

[edit]

In 2021, a team of researchers used Lean to verify the correctness of a proof by Peter Scholze in the area of condensed mathematics. The project garnered attention for formalizing a result at the cutting edge of mathematical research.[21] In 2023, Terence Tao used Lean to formalize a proof of the Polynomial Freiman-Ruzsa (PFR) conjecture, a result published by Tao and collaborators in the same year.[22]

### Artificial intelligence

[edit]

In 2022, OpenAI and Meta AI independently created AI models to generate proofs of various high-school-level olympiad problems in Lean.[23] Meta AI's model is available for public use with the Lean environment.[24]

In 2023, Vlad Tenev and Tudor Achim co-founded startup Harmonic, which aims to reduce AI hallucinations by generating and checking Lean code.[25]

In 2024, Google DeepMind created AlphaProof[26] which proves mathematical statements in Lean at the level of a silver medalist at the International Mathematical Olympiad. This was the first AI system that achieved a medal-worthy performance on a math olympiad's problems.[27]

In April 2025, DeepSeek introduced DeepSeek-Prover-V2, an AI model designed for theorem proving in Lean 4, built on top of DeepSeek-V3.[28]

## See also

[edit]

* Mathematics portal
* Free and open-source software portal

* Dependent type
* List of proof assistants
* mimalloc
* Type theory

## References

[edit]

1. ^ "Release 4.21.0". 30 June 2025. Retrieved 22 July 2025.
2. ^ a b Moura, Leonardo de; Ullrich, Sebastian (2021). "The Lean 4 Theorem Prover and Programming Language". In Platzer, André; Sutcliffe, Geoff (eds.). Automated Deduction – CADE 28. Lecture Notes in Computer Science. Vol. 12699\. Cham: Springer International Publishing. pp. 625–635\. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5.
3. ^ "About". Lean Language. Retrieved 2024-03-13.
4. ^ Moura, Leonardo de; Ullrich, Sebastian (2021). Platzer, Andr'e; Sutcliffe, Geoff (eds.). Automated Deduction -- CADE 28. Springer International Publishing. pp. 625–635\. doi:10.1007/978-3-030-79876-5_37. ISBN 978-3-030-79876-5. S2CID 235800962. Retrieved 24 March 2023.
5. ^ "Significant changes from Lean 3". Lean Manual. Retrieved 24 March 2023.
6. ^ "Mission". Lean FRO. 2023-07-25. Retrieved 2024-03-14.
7. ^ "Programming Languages Software Award". www.sigplan.org. Archived from the original on 6 Jul 2025. Retrieved 2025-07-06.
8. ^ "batteries". GitHub. Retrieved 2024-09-22.
9. ^ "Building the Mathematical Library of the Future". Quanta Magazine. October 2020. Archived from the original on 2 Oct 2020.
10. ^ "Lean community". leanprover-community.github.io. Retrieved 2023-10-24.
11. ^ "Mathlib statistics". leanprover-community.github.io. Retrieved 2025-05-07.
12. ^ "Installing Lean 4 on Linux". leanprover-community.github.io. Retrieved 2023-10-24.
13. ^ Hales, Thomas (September 18, 2018). "A Review of the Lean Theorem Prover". Jigger Wit. Archived from the original on 21 Nov 2020.
14. ^ Buzzard, Kevin. "The Future of Mathematics?" (PDF). Retrieved 6 October 2020.
15. ^ Tao, Terence (31 May 2025). "A Lean companion to "Analysis I"". Terry Tao -- What's New. WordPress. Archived from the original on 31 May 2025.
16. ^ Macbeth, Heather. "The Mechanics of Proof". hrmacbeth.github.io. Archived from the original on 5 Jun 2024.
17. ^ "Formal Abstracts". Github.
18. ^ "What is the Xena project?". Xena. 8 May 2019.
19. ^ Tao, Terence. "analysis". github.com/teorth.
20. ^ Roberts, Siobhan (July 2, 2023). "A.I. Is Coming for Mathematics, Too". New York Times. Archived from the original on 1 May 2024.
21. ^ Hartnett, Kevin (July 28, 2021). "Proof Assistant Makes Jump to Big-League Math". Quanta Magazine. Archived from the original on 2 Jan 2022.
22. ^ Sloman, Leila (2023-12-06). "'A-Team' of Math Proves a Critical Link Between Addition and Sets". Quanta Magazine. Retrieved 2023-12-07.
23. ^ "Solving (some) formal math olympiad problems". OpenAI. February 2, 2022. Retrieved March 13, 2024.
24. ^ "Teaching AI advanced mathematical reasoning". Meta AI. November 3, 2022. Retrieved March 13, 2024.
25. ^ Metz, Cade (23 September 2024). "Is Math the Path to Chatbots That Don't Make Stuff Up?". New York Times. Archived from the original on 24 Sep 2024.
26. ^ "AI achieves silver-medal standard solving International Mathematical Olympiad problems". Google DeepMind. 2024-05-14. Retrieved 2024-07-25.
27. ^ Roberts, Siobhan (July 25, 2024). "Move Over, Mathematicians, Here Comes AlphaProof". New York Times. Archived from the original on July 29, 2024.
28. ^ "DeepSeek upgrades its math-focused AI model Prover". Yahoo Finance. April 30, 2025. Retrieved April 30, 2025.

## External links

[edit]

* Lean Website
* Lean Community Website
* Lean FRO
* The Natural Number Game \- an interactive tutorial to learn Lean
* Moogle.ai \- a semantic search engine for finding theorems in mathlib

* v
* t
* e

Microsoft free and open-source software (FOSS)

Overview|

* Microsoft and open source
* Shared Source Initiative

Software|

| Applications|

* 3D Movie Maker
* Atom
* Conference XP
* Family.Show
* File Manager
* Open Live Writer
* Microsoft Edit
* Microsoft PowerToys
* Terminal
* Windows Calculator
* Windows Console
* Windows Package Manager
* WorldWide Telescope
* XML Notepad

|

Video games|

* Allegiance

Programming
languages|

* Bosque
* C#
* Dafny
* F#
* F*
* GW-BASIC
* IronPython
* IronRuby
* Lean
* P
* Power Fx
* PowerShell
* Project Verona
* Q#
* Small Basic Online
* TypeScript
* Visual Basic

Frameworks,
development tools|

* .NET
* .NET Framework
* .NET Gadgeteer
* .NET MAUI
* .NET Micro Framework
* AirSim
* ASP.NET
* ASP.NET AJAX
* ASP.NET Core
* ASP.NET MVC
* ASP.NET Razor
* ASP.NET Web Forms
* Avalonia
* Babylon.js
* BitFunnel
* Blazor
* C++/WinRT
* CCF
* ChakraCore
* CLR Profiler
* Dapr
* DeepSpeed
* DiskSpd
* Dryad
* Dynamic Language Runtime
* eBPF on Windows
* Electron
* Entity Framework
* Fluent Design System
* Fluid Framework
* Infer.NET
* LightGBM
* Managed Extensibility Framework
* Microsoft Automatic Graph Layout
* Microsoft C++ Standard Library
* Microsoft Cognitive Toolkit
* Microsoft Design Language
* Microsoft Detours
* Microsoft Enterprise Library
* Microsoft SEAL
* mimalloc
* Mixed Reality Toolkit
* ML.NET
* mod_mono
* Mono
* MonoDevelop
* MSBuild
* MsQuic
* Neural Network Intelligence
* npm
* NuGet
* OneFuzz
* Open Management Infrastructure
* Open Neural Network Exchange
* Open Service Mesh
* Open XML SDK
* Orleans
* Playwright
* ProcDump
* ProcMon
* Python Tools for Visual Studio
* R Tools for Visual Studio
* RecursiveExtractor
* Roslyn
* Sandcastle
* SignalR
* StyleCop
* SVNBridge
* T2 Temporal Prover
* Text Template Transformation Toolkit
* TLA+ Toolbox
* U-Prove
* vcpkg
* Virtual File System for Git
* Voldemort
* VoTT
* Vowpal Wabbit
* Windows App SDK
* Windows Communication Foundation
* Windows Driver Frameworks
* KMDF
* UMDF
* Windows Forms
* Windows Presentation Foundation
* Windows Template Library
* Windows UI Library
* WinJS
* WinObjC
* WiX
* XDP for Windows
* XSP
* xUnit.net
* Z3 Theorem Prover

Operating systems|

* MS-DOS (v1.25, v2.0 & v4.0)
* Barrelfish
* SONiC
* Azure Linux

Other|

* ChronoZoom
* Extensible Storage Engine
* FlexWiki
* FourQ
* Gollum
* Project Mu
* ReactiveX
* SILK
* TLAPS
* TPM 2.0 Reference Implementation
* WikiBhasha
* Windows Subsystem for Linux

Licenses|

* Microsoft Public License
* Microsoft Reciprocal License

Forges|

* CodePlex
* GitHub

Related|

* .NET Foundation
* F# Software Foundation
* Microsoft Open Specification Promise
* Open Letter to Hobbyists
* Open Source Security Foundation
* Outercurve Foundation

Category

* v
* t
* e

Microsoft development tools

Development
environments|

| Visual Studio|

* Code
* Express
* Team System Profiler
* Tools for Applications
* Tools for Office

|

Others|

* Blend
* Expression Web
* FxCop
* GW-BASIC
* MACRO-80
* Macro Assembler
* MSBuild
* Pascal
* QuickBASIC
* QBasic
* QuickC
* Robotics Developer Studio
* Roslyn
* SharePoint Designer
* FrontPage
* Small Basic
* WebMatrix
* Windows App SDK
* Windows App Studio
* Windows SDK
* CLR Profiler
* ILAsm
* Native Image Generator
* WinDiff
* XAMLPad

Languages|

* Dynamics AX
* BASIC
* Visual Basic
* legacy
* VB.NET
* VBA
* VBScript
* Bosque
* Visual C++
* C++/CX
* C++/CLI
* Managed C++
* C++/WinRT
* C#
* C/AL
* Dafny
* Dexterity
* F#
* F*
* Visual FoxPro
* Java
* J++
* J#
* JavaScript
* TypeScript
* JScript
* IronPython
* IronRuby
* Lean
* P
* Power Fx
* PowerShell
* Project Verona
* Q#
* Small Basic
* VPL
* XAML

APIs and
frameworks|

| Native|

* Windows API
* Silverlight
* XNA
* DirectX
* Managed DirectX
* UWP
* Xbox Development Kit
* Windows Installer
* WinUI

|

.NET|

* ASP.NET
* Core
* AJAX
* Dynamic Data
* MVC
* Razor
* Web Forms
* ADO.NET
* Entity Framework
* MAUI
* CardSpace
* Communication Foundation
* Identity Foundation
* LINQ
* Presentation Foundation
* Workflow Foundation

Device drivers|

* WDK
* WDF
* KMDF
* UMDF
* Windows HLK
* WDM

Database|

| SQL Server|

* Express
* Compact
* Management Studio
* MSDE

|

SQL services|

* Analysis
* Reporting
* Integration
* Notification

Other|

* Visual FoxPro
* Microsoft Access
* Access Database Engine
* Extensible Storage Engine

Source control|

* Visual SourceSafe
* Team Foundation Version Control

Testing and
debugging|

* CodeView
* OneFuzz
* Playwright
* Script Debugger
* WinDbg
* xUnit.net

Delivery|

* Active Setup
* ClickOnce
* npm
* NuGet
* vcpkg
* Web Platform Installer
* Windows Installer
* WiX
* Windows Package Manager
* Microsoft Store

Category

* v
* t
* e

Microsoft Research (MSR)

Main
projects|

| Languages, compilers|

* Bartok
* Bosque
* Cω
* F*
* Lean
* P
* Project Verona
* Phoenix
* Polyphonic C#
* SecPAL

|

Distributed–grid computing|

* BitVault
* Confidential Consortium Framework
* DeepSpeed
* Orleans

Internet, networking|

* AjaxView
* Avalanche
* Conference XP
* Gazelle
* HoneyMonkey
* Penny Black
* Wallop
* WikiBhasha

Other projects|

* Automatic Graph Layout
* Cognitive Toolkit
* Digits
* Holoportation
* IllumiRoom
* Image Composite Editor
* Infer.NET
* LightGBM
* LiveStation
* MyLifeBits
* Neural Network Intelligence
* NodeXL
* OneFuzz
* PhotoDNA
* SEAL
* SLAM
* T2 Temporal Prover
* WorldWide Telescope
* Z3 Theorem Prover

Operating systems|

* Barrelfish
* HomeOS
* Midori
* Singularity
* Verve

APIs|

* Accelerator
* Dryad
* Joins
* mimalloc

Launched as products|

* C#
* Comic Chat
* Detours
* F#
* Sideshow
* PixelSense (TouchLight)
* SenseCam
* ClearType
* Group Shot
* Allegiance
* TrueSkill
* Songsmith
* Xbox
* Kinect

MSR Labs
applied
research|

| Live Labs|

| Current|

* Pivot
* Seadragon
* Deep Zoom

|

Discontinued|

* Deepfish
* Listas
* Live Clipboard
* Photosynth

FUSE Labs|

* Docs.com
* Kodu

Other labs|

* Academic Search
* adCenter Labs
* Office Labs

Category
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template