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.

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

In this interim period members of the Lean community developed and released unofficial versions up to 3.51.1.

[4] Lean 4 also contains a macro system and improved type class synthesis and memory management procedures over the previous version.

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

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

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

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