View source for Lean (proof assistant)

{{short description|Proof assistant and programming language}}
{{Infobox programming language
| name = Lean
| logo = Lean logo2.svg
| paradigm = [[Functional programming]], [[Imperative programming]]
| developer = [https://lean-fro.org/ Lean FRO]
| released = {{Start date and age|2013}}
| latest release version = {{wikidata|property|edit|reference|P548=Q2804309|P348}}
| latest release date = {{Start date and age|{{wikidata|qualifier|P548=Q2804309|P348|P577}}|df=yes}}
| programming language = Lean, [[C++]]
| typing = [[static typing|Static]], [[strong and weak typing|strong]], [[type inference|inferred]]
| platform = 
| operating system = [[Cross-platform]]
| family = [[Proof assistant]]
| license = [[Apache License 2.0]]
| website = {{URL|https://lean-lang.org/}}
| influenced = 
| influenced_by = [[ML (programming language)|ML]]<br>[[Coq (software)|Coq]]<br>[[Haskell]]
}}

'''Lean''' is a [[proof assistant]] and a [[Functional programming|functional programming language]].<ref name=":0">{{Cite book |last1=Moura |first1=Leonardo de |last2=Ullrich |first2=Sebastian |date=2021 |editor-last=Platzer |editor-first=André |editor2-last=Sutcliffe |editor2-first=Geoff |chapter=The Lean 4 Theorem Prover and Programming Language |title=Automated Deduction – CADE 28 |series=Lecture Notes in Computer Science |volume=12699 |language=en |location=Cham |publisher=Springer International Publishing |pages=625–635 |doi=10.1007/978-3-030-79876-5_37 |isbn=978-3-030-79876-5|doi-access=free }}</ref> It is based on the [[calculus of constructions]] with [[inductive type]]s. It is an [[open-source]] project hosted on [[GitHub]]. It 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. Development is currently supported by the [[Nonprofit organization|non-profit]] Lean [[Focused Research Organization|Focused Research Organization (FRO)]].

== History ==
Lean was launched by Leonardo de Moura at [[Microsoft Research]] in 2013.<ref>{{Cite web |title=About |url=https://lean-lang.org/about/ |access-date=2024-03-13 |website=Lean Language}}</ref> 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 (programming language)|C]] code which is then compiled, enabling the development of efficient domain-specific automation.<ref>{{cite book |last1=Moura |first1=Leonardo de |last2=Ullrich |first2=Sebastian |editor1-last=Platzer |editor1-first=Andr'e |editor2-last=Sutcliffe |editor2-first=Geoff |title=Automated Deduction -- CADE 28 |date=2021 |publisher=Springer International Publishing |isbn=978-3-030-79876-5 |pages=625–635 |doi=10.1007/978-3-030-79876-5_37 |s2cid=235800962 |url=https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37 |access-date=24 March 2023}}</ref> 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.<ref name=":0" />

Lean 4 is not [[Backward compatibility|backwards-compatible]] with Lean 3.<ref>{{cite web |title=Significant changes from Lean 3 |url=https://leanprover.github.io/lean4/doc/lean3changes.html |website=Lean Manual |access-date=24 March 2023}}</ref>

In 2023, the Lean FRO was formed, with the goals of improving the language's scalability and usability, and implementing [[proof automation]].<ref>{{Cite web |date=2023-07-25 |title=Mission |url=https://lean-fro.org/about/ |access-date=2024-03-14 |website=Lean FRO}}</ref>

== Overview ==
=== Libraries ===

The official lean package includes a [[standard library]] ''batteries'', which implements common [[data structure]]s that may be used for both mathematical research and more conventional software development.<ref>{{Cite web |title=batteries |url=https://github.com/leanprover-community/batteries |access-date=2024-09-22 |website=[[GitHub]]}}</ref>

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.<ref>{{Cite web |title=Building the Mathematical Library of the Future |url=https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ |archive-url=https://archive.today/20201002043743/https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ |archive-date=2 Oct 2020 |website=[[Quanta Magazine]]|date=October 2020 }}</ref><ref>{{Cite web |title=Lean community |url=https://leanprover-community.github.io/lean3/ |access-date=2023-10-24 |website=leanprover-community.github.io}}</ref> As of September 2024, mathlib had formalized over 165,000 theorems and 85,000 definitions in Lean.<ref>{{Cite web |title=Mathlib statistics |url=https://leanprover-community.github.io/mathlib_stats.html |access-date=2024-09-22 |website=leanprover-community.github.io}}</ref>

=== Editors integration ===

Lean integrates with:<ref>{{Cite web |title=Installing Lean 4 on Linux |url=https://leanprover-community.github.io/install/linux.html |access-date=2023-10-24 |website=leanprover-community.github.io}}</ref>

* [[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)==

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 function|successor]] of some other natural number.
<syntaxhighlight lang="lean">
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
</syntaxhighlight>

Addition of natural numbers can be [[Recursive definition|defined recursively]], using [[pattern matching]]. 
<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

This is a simple proof of <math>(P \wedge Q) \implies (Q \wedge P)</math> for two [[proposition]]s {{mvar|P}} and {{mvar|Q}} (where {{and}} is the [[Logical conjunction|conjunction]] and <math>\implies</math> the [[Material conditional|implication]]) in Lean using tactic mode:
<syntaxhighlight lang="lean4">
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
</syntaxhighlight>

This same proof in term mode:
<syntaxhighlight lang="lean4">
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
    fun ⟨hp, hq⟩ => ⟨hq, hp⟩
</syntaxhighlight>

== Usage ==

=== Mathematics ===
{{See also|Proof assistant#Notable formalized proofs}}

Lean has received attention from mathematicians such as [[Thomas Callister Hales|Thomas Hales]],<ref>{{Cite web |last=Hales |first=Thomas |date=September 18, 2018 |title=A Review of the Lean Theorem Prover |url=https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ |archive-url=https://archive.today/20201121125544/https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ |archive-date=21 Nov 2020 |website=Jigger Wit}}</ref> [[Kevin Buzzard]],<ref name="Buzzard" /> and Heather Macbeth.<ref>{{Cite web |last=Macbeth |first=Heather |title=The Mechanics of Proof |url=https://hrmacbeth.github.io/math2001/ |archive-url=https://archive.today/20240605090236/https://hrmacbeth.github.io/math2001/ |archive-date=5 Jun 2024 |website=hrmacbeth.github.io}}</ref> Hales is using it for his project, Formal Abstracts.<ref>{{cite web |title=Formal Abstracts |url=https://formalabstracts.github.io/ |website=Github}}</ref> Buzzard uses it for the Xena project.<ref>{{cite web |title=What is the Xena project? |url=https://xenaproject.wordpress.com/what-is-the-xena-project/ |website=Xena |language=en |date=8 May 2019}}</ref> 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. Macbeth is using Lean to teach students the fundamentals of mathematical proof with instant feedback.<ref>{{Cite web |last=Roberts |first=Siobhan |date=July 2, 2023 |title=A.I. Is Coming for Mathematics, Too |url=https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html |archive-url=https://archive.today/20240501080422/https://www.nytimes.com/2023/07/02/science/ai-mathematics-machine-learning.html |archive-date=1 May 2024 |website=New York Times}}</ref>

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.<ref name="Quanta21">{{cite news |last=Hartnett |first=Kevin |date=July 28, 2021 |title=Proof Assistant Makes Jump to Big-League Math |work=[[Quanta Magazine]] |url=https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ |archive-url=https://archive.today/20220102145317/https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/ |archive-date=2 Jan 2022}}</ref> In 2023, [[Terence Tao]] used Lean to formalize a proof of the [[Freiman's theorem|Polynomial Freiman-Ruzsa]] (PFR) conjecture, a result published by Tao and collaborators in the same year.<ref>{{Cite web |last=Sloman |first=Leila |date=2023-12-06 |title='A-Team' of Math Proves a Critical Link Between Addition and Sets |url=https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ |access-date=2023-12-07 |website=Quanta Magazine |language=en}}</ref>

=== Artificial intelligence ===
In 2022, [[OpenAI]] and [[Meta AI]] independently created AI models to generate proofs of various high-school-level olympiad problems in Lean.<ref>{{Cite web |date=February 2, 2022 |title=Solving (some) formal math olympiad problems |url=https://openai.com/research/formal-math |access-date=March 13, 2024 |website=[[OpenAI]]}}</ref> Meta AI's model is available for public use with the Lean environment.<ref>{{Cite web |date=November 3, 2022 |title=Teaching AI advanced mathematical reasoning |url=https://ai.meta.com/blog/ai-math-theorem-proving/ |access-date=March 13, 2024 |website=[[Meta AI]]}}</ref>

In 2023, [[Vlad Tenev]] and Tudor Achim co-founded startup Harmonic, which aims to reduce [[Hallucination (artificial intelligence)|AI hallucinations]] by generating and checking Lean code.<ref>{{Cite news |last=Metz |first=Cade |date=23 September 2024 |title=Is Math the Path to Chatbots That Don't Make Stuff Up? |url=https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html |archive-url=https://archive.today/20240924084639/https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html |archive-date=24 Sep 2024 |work=New York Times}}</ref>

In 2024, [[Google DeepMind]] created [[Google DeepMind#AlphaProof|AlphaProof]]<ref>{{Cite web |date=2024-05-14 |title=AI achieves silver-medal standard solving International Mathematical Olympiad problems |url=https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ |access-date=2024-07-25 |website=Google DeepMind |language=en}}</ref> 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.<ref>{{Cite web |last=Roberts |first=Siobhan |date=July 25, 2024 |title=Move Over, Mathematicians, Here Comes AlphaProof |url=https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html |archive-url=https://archive.today/20240729121148/https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html |archive-date=July 29, 2024 |website=[[New York Times]]}}</ref>

==See also==
{{Portal|Mathematics|Free and open-source software}}
* [[Dependent type]]
* [[List of proof assistants]]
* [[mimalloc]]
* [[Type theory]]

==References==
{{reflist|refs=
<!-- <ref name="Hales">{{cite web |last1=Hales |first1=Thomas |title=A Review of the Lean Theorem Prover |date=18 September 2018 |url=https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/ |access-date=6 October 2020}}</ref>-->
<ref name="Buzzard">{{cite web |last1=Buzzard |first1=Kevin |title=The Future of Mathematics? |url=https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf |access-date=6 October 2020}}</ref> 
}}

==External links==
* [https://leanprover.github.io/ Lean Website]
* [https://leanprover-community.github.io/ Lean Community Website]
* [https://lean-fro.org Lean FRO]
* [https://adam.math.hhu.de/#/g/leanprover-community/nng4 The Natural Number Game] - an interactive tutorial to learn Lean
* [https://www.moogle.ai/ Moogle.ai] - a semantic search engine for finding theorems in mathlib

{{Microsoft FOSS}}
{{Microsoft development tools}}
{{Microsoft Research}}

[[Category:Programming languages created in 2013]]
[[Category:Proof assistants]]
[[Category:Dependently typed languages]]
[[Category:Educational math software]]
[[Category:Functional languages]]
[[Category:Free and open-source software]]
[[Category:Free software programmed in C++]]
[[Category:Microsoft free software]]
[[Category:Microsoft programming languages]]
[[Category:Microsoft Research]]
[[Category:Software using the Apache license]]
[[Category:Free mathematics software|Theorem provers]]
[[Category:Theorem proving software systems]]