Originally launched by Leonardo de Moura at Microsoft Research in 2013, versions 1 and 2 of Lean were experimental, while version 3 was the first semi-stable release of the Lean programming language, and version 4 is not backward-compatible with version 3.
With its first stable release in 2023, Lean 4, a fully stable version of the language, offers significant benefits over Lean 4.
ML, Coq, and Haskell influenced lean.
Based on a calculus of constructions with inductive types, Lean was created as a proof assistant and programming language. The first two versions were considered experimental and included features such as support for Homotopy Type Theory based foundations that were later dropped.
Lean 3 was implemented primarily in C++ with some features written in Lean. After version 3.4.2, Lean 3 was officially end-of-lifed while Lean 4 began, as Lean 4 was not intended to be compatible with previous versions. During this period, members of the Lean Community developed and released unofficial versions up to 3.51.1.
Lean 4, which was released in 2021, is a reimplementation of the Lean theorem prover. It is capable of producing C code that can be compiled, enabling the development of efficient domain-specific automation. Lean 4 includes a macro system and improved typeclass synthesis and memory management procedures over the previous version. Additionally, Lean 4 allows users to modify the frontend and other key parts of the core system without touching C++ code, as they are now all implemented in Lean and available to the end user to be overridden as needed.
The Lean mathematical library, mathlib, is a community-driven effort to build a library of mathematics formalized in the Lean proof assistant. It also contains definitions useful in programming.
A proof assistant is a piece of software that provides a language for defining objects, specifying properties of these objects, and proving that these specifications hold. The system checks to determine that these proofs are correct down to their logical foundation. Proof assistants are often used to verify the correctness of a program, but they can also be used for abstract mathematics, which is of particular interest to the mathlib community.
Up to version 3, Lean focused on being a proof assistant, and its chief applications have been to digitize theoretical mathematics. However, a goal of Lean 4 is to make Lean a good programming language rather than just a proof assistant. To that end, its syntax has been reworked in several ways to make it easier to write a wider variety of programs. An optimizing compiler that generates efficient C code was written, making it easier to integrate with C/C++ code when necessary. Lean 4 is largely self-hosting and written in Lean itself.
This portion of our web guide is dedicated to the Lean programming language. Topics related to the language itself, or any compilers, editors, IDEs, or other tools or utilities designed to facilitate programming with Lean, are appropriate for this category, as are Lean programming guides, tutorials, communities, or forums.
Recommended Resources
This is the official GitHub repository for the Lean 4 programming language and theorem prover. Maintained by the Lean Prover Community, the repository contains the source code for Lean 4, a dependently typed programming language and theorem prover. The repository offers a to help users set up Lean 4 and use it with VS Code as an editor, as well as links to several other resources, such as tutorials, examples, release notes, forks, and branches. Lean 4 is available under an Apache 2.0 license.
https://github.com/leanprover/lean4
Hosted on GitHub, this is a community chat platform for the Lean Community, and about the Lean interactive theorem prover. Members of the Lean Community, who are actively involved in the active development of the Lean programming language and theorem prover, as well as others who have an interest in the software. Zulip, the chat platform, is designed to help teams communicate more efficiently and productively, presenting messages in context regardless of when it was posted.
https://leanprover.zulipchat.com/
This is the official website of the Lean Community, involved in the development of the Lean programming language, its mathlib library, and other Lean infrastructure, including the Lean theorem prover, which is an interactive theorem prover used to construct formal proofs that are open-source and hosted on GitHub. Community issues, papers, and projects are featured, along with installation instructions, documentation, library overviews, and downloads of Lean and related files.
https://leanprover-community.github.io
Developed as part of the project ADAM: Anticipating the Digital Age of Mathematics at Heinrich-Heine-Universität in Düsseldorf, this is a repository of learning games for the proof assistant Lean 4 and its mathematical library "mathlib," Available games include a classical introduction game for the Lean programming language, a game about set theory, and an introduction to constructive logic using Lean, and some other games in languages other than English.
https://adam.math.hhu.de/
Lean is a theorem prover and programming language that was launched by Leonardo de Moura at Microsoft Research in 2013, and is currently, an open-source project hosted on GitHub, and available under the Apache 2.0 license. Binary packages are available for all major platforms, and the source code can be downloaded. Documentation, a list of publications, most of which can be downloaded in PDF format, and links to a Lean chat room, and profiles of the people involved in its development are posted.
https://leanprover.github.io/
Created by Kevin Buzzard and Mohammad Pedramfar, this is a part-book, part-game, designed to show the power of induction, created to demonstrate a program written for version 3 of the Lean programming language. The game may be played online, and instructions for the game are presented, along with its purpose and additional information in a FAQ. The game utilizes the Lean 3 interactive theorem prover, also making use of a Lean-to-HTML formatter created by Patrick Massot.
https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/index2.html
Using Lean as a Programming Language
In the context of the repository for a Carnegie Mellon University course that introduces symbolic logic on three levels: theory, implementation, and application, a tutorial on using Lean 3 as a programming language is provided. Keeping in mind that version 3 was not yet considered a fully functional programming language, this offers information detailing how it nevertheless could function as such. Coding exercises and links to other online resources are provided.
https://avigad.github.io/lamr/using_lean_as_a_programming_language.html
