Lean (proof assistant)

Last updated
Lean
Lean logo2.svg
Paradigm Functional programming, Imperative programming
Family Proof assistant
Developer Lean FRO
First appeared2013;12 years ago (2013)
Stable release
4.14.0 [1]   OOjs UI icon edit-ltr-progressive.svg / 1 December 2024;37 days ago (1 December 2024)
Typing discipline Static, strong, inferred
Implementation languageLean, C++
OS Cross-platform
License Apache License 2.0
Website lean-lang.org
Influenced by
ML
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. 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 non-profit Lean Focused Research Organization (FRO).

Contents

History

Lean 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.[ citation needed ]

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]

Overview

Libraries

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

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. [8] [9] As of September 2024, mathlib had formalised over 165,000 theorems and 85,000 definitions in Lean. [10]

Editors integration

Lean integrates with: [11]

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 of some other natural number.

inductiveNat:Type|zero:Nat|succ:Nat→Nat

Addition of natural numbers can be defined recursively, using pattern matching. 

defNat.add:Nat→Nat→Nat|n,Nat.zero=>n-- n + 0 = n  |n,Nat.succm=>Nat.succ(Nat.addnm)-- n + succ(m) = succ(n + m)

This is a simple proof of for two propositions P and Q (where is the conjunction and 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

Mathematics

Lean has received attention from mathematicians such as Thomas Hales, [12] Kevin Buzzard, [13] and Heather Macbeth. [14] Hales is using it for his project, Formal Abstracts. [15] Buzzard uses it for the Xena project. [16] 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. [17]

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. [18] 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. [19]

Artificial intelligence

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

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

In 2024, Google DeepMind created AlphaProof [23] 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. [24]

See also

Related Research Articles

<span class="mw-page-title-main">Gregory Chaitin</span> Argentine-American mathematician

Gregory John Chaitin is an Argentine-American mathematician and computer scientist. Beginning in the late 1960s, Chaitin made contributions to algorithmic information theory and metamathematics, in particular a computer-theoretic result equivalent to Gödel's incompleteness theorem. He is considered to be one of the founders of what is today known as algorithmic complexity together with Andrei Kolmogorov and Ray Solomonoff. Along with the works of e.g. Solomonoff, Kolmogorov, Martin-Löf, and Leonid Levin, algorithmic information theory became a foundational part of theoretical computer science, information theory, and mathematical logic. It is a common subject in several computer science curricula. Besides computer scientists, Chaitin's work draws attention of many philosophers and mathematicians to fundamental problems in mathematical creativity and digital philosophy.

OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

In combinatorics, Ramsey's theorem, in one of its graph-theoretic forms, states that one will find monochromatic cliques in any edge labelling (with colours) of a sufficiently large complete graph. To demonstrate the theorem for two colours (say, blue and red), let r and s be any two positive integers. Ramsey's theorem states that there exists a least positive integer R(r, s) for which every blue-red edge colouring of the complete graph on R(r, s) vertices contains a blue clique on r vertices or a red clique on s vertices. (Here R(r, s) signifies an integer that depends on both r and s.)

The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically.

<span class="mw-page-title-main">Timothy Gowers</span> British mathematician

Sir William Timothy Gowers, is a British mathematician. He is Professeur titulaire of the Combinatorics chair at the Collège de France, and director of research at the University of Cambridge and Fellow of Trinity College, Cambridge. In 1998, he received the Fields Medal for research connecting the fields of functional analysis and combinatorics.

In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs from a hypothesis in systems that do not explicitly axiomatize that hypothesis, i.e. to prove an implication A → B, it is sufficient to assume A as a hypothesis and then proceed to derive B. Deduction theorems exist for both propositional logic and first-order logic. The deduction theorem is an important tool in Hilbert-style deduction systems because it permits one to write more comprehensible and usually much shorter proofs than would be possible without it. In certain other formal proof systems the same conveniency is provided by an explicit inference rule; for example natural deduction calls it implication introduction.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human–machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human–machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.

In additive combinatorics, a discipline within mathematics, Freiman's theorem is a central result which indicates the approximate structure of sets whose sumset is small. It roughly states that if is small, then can be contained in a small generalized arithmetic progression.

<span class="mw-page-title-main">Thomas Callister Hales</span> American mathematician

Thomas Callister Hales is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification. In representation theory he is known for his work on the Langlands program and the proof of the fundamental lemma over the group Sp(4). In discrete geometry, he settled the Kepler conjecture on the density of sphere packings, the honeycomb conjecture, and the dodecahedral conjecture. In 2014, he announced the completion of the Flyspeck Project, which formally verified the correctness of his proof of the Kepler conjecture.

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer.

In combinatorial number theory, the Erdős–Graham problem is the problem of proving that, if the set of integers greater than one is partitioned into finitely many subsets, then one of the subsets can be used to form an Egyptian fraction representation of unity. That is, for every , and every -coloring of the integers greater than one, there is a finite monochromatic subset of these integers such that

Peter Benedict Kronheimer is a British mathematician, known for his work on gauge theory and its applications to 3- and 4-dimensional topology. He is William Caspar Graustein Professor of Mathematics at Harvard University and former chair of the mathematics department.

<span class="mw-page-title-main">Kevin Buzzard</span> British mathematician

Kevin Mark Buzzard is a British mathematician and currently a professor of pure mathematics at Imperial College London. He specialises in arithmetic geometry and the Langlands program.

In category theory, a branch of mathematics, Grothendieck's homotopy hypothesis states that the ∞-groupoids are spaces.

Univalent foundations are an approach to the foundations of mathematics in which mathematical structures are built out of objects called types. Types in univalent foundations do not correspond exactly to anything in set-theoretic foundations, but they may be thought of as spaces, with equal types corresponding to homotopy equivalent spaces and with equal elements of a type corresponding to points of a space connected by a path. Univalent foundations are inspired both by the old Platonic ideas of Hermann Grassmann and Georg Cantor and by "categorical" mathematics in the style of Alexander Grothendieck. Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory. The development of univalent foundations is closely related to the development of homotopy type theory.

Condensed mathematics is a theory developed by Dustin Clausen and Peter Scholze which replaces a topological space by a certain sheaf of sets, in order to solve some technical problems of doing homological algebra on topological groups.

<span class="mw-page-title-main">Meta AI</span> Artificial intelligence division of Meta Platforms

Meta AI is a company owned by Meta that develops artificial intelligence and augmented and artificial reality technologies. Meta AI deems itself an academic research laboratory, focused on generating knowledge for the AI community, and should not be confused with Meta's Applied Machine Learning (AML) team, which focuses on the practical applications of its products.

References

  1. ↑ "Release 4.14.0". 1 December 2024. Retrieved 26 December 2024.
  2. ↑ 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. ↑ "batteries". GitHub . Retrieved 2024-09-22.
  8. ↑ "Building the Mathematical Library of the Future". Quanta Magazine . October 2020. Archived from the original on 2 Oct 2020.
  9. ↑ "Lean community". leanprover-community.github.io. Retrieved 2023-10-24.
  10. ↑ "Mathlib statistics". leanprover-community.github.io. Retrieved 2024-09-22.
  11. ↑ "Installing Lean 4 on Linux". leanprover-community.github.io. Retrieved 2023-10-24.
  12. ↑ Hales, Thomas (September 18, 2018). "A Review of the Lean Theorem Prover". Jigger Wit. Archived from the original on 21 Nov 2020.
  13. ↑ Buzzard, Kevin. "The Future of Mathematics?" (PDF). Retrieved 6 October 2020.
  14. ↑ Macbeth, Heather. "The Mechanics of Proof". hrmacbeth.github.io. Archived from the original on 5 Jun 2024.
  15. ↑ "Formal Abstracts". Github.
  16. ↑ "What is the Xena project?". Xena. 8 May 2019.
  17. ↑ Roberts, Siobhan (July 2, 2023). "A.I. Is Coming for Mathematics, Too". New York Times. Archived from the original on 1 May 2024.
  18. ↑ Hartnett, Kevin (July 28, 2021). "Proof Assistant Makes Jump to Big-League Math". Quanta Magazine . Archived from the original on 2 Jan 2022.
  19. ↑ Sloman, Leila (2023-12-06). "'A-Team' of Math Proves a Critical Link Between Addition and Sets". Quanta Magazine. Retrieved 2023-12-07.
  20. ↑ "Solving (some) formal math olympiad problems". OpenAI . February 2, 2022. Retrieved March 13, 2024.
  21. ↑ "Teaching AI advanced mathematical reasoning". Meta AI . November 3, 2022. Retrieved March 13, 2024.
  22. ↑ 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.
  23. ↑ "AI achieves silver-medal standard solving International Mathematical Olympiad problems". Google DeepMind. 2024-05-14. Retrieved 2024-07-25.
  24. ↑ Roberts, Siobhan (July 25, 2024). "Move Over, Mathematicians, Here Comes AlphaProof". New York Times . Archived from the original on July 29, 2024.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.