What is Lean written in?

Software for interactive and automated theorem proving.

Programming language Year 2013 Paradigm functional, proof-assistant, dependent-typed Typing static Self-hosting yes
Its runtime is implemented in C++ (documented). Lean is self-hosting.

Quick Facts

Designed by
Leonardo de Moura
Developer
Microsoft Research
First released
2013
Typing
static
License
Apache Software License 2.0
Website
lean-lang.org

About Lean

Lean is a software for interactive and automated theorem proving. It is a statically typed and garbage-collected language that compiles ahead of time to native machine code. It supports functional, proof-assistant, and dependent-typed programming.

Lean first appeared in 2013 and was designed by Leonardo de Moura. Development is led by Microsoft Research. Lean is now used mainly in specialized niches and by dedicated communities.

How Lean is implemented

In the Language Lineage dataset, Lean is self-hosting, so its own compiler is written in Lean itself and its runtime is implemented in C++. Reaching self-hosting — where a language is mature enough to compile itself — is a milestone that proves the language can handle a large, real-world program.

Lean in the language family tree

Lean drew on ideas from Coq and Haskell.

Sources: Wikipedia · Wikidata · Official site

Relationship Graph

All directly connected languages. Click any node to navigate to its page.

Runtime Implementation

LanguageConfidenceNotesSource
C++ 85% Lean 4 compiles via a C backend and a C++ runtime. Source

Influenced By

Frequently Asked Questions

What language is Lean written in?
Lean is primarily implemented in C++. See the implementation section above for details and source references.
What languages influenced Lean?
Lean was influenced by Coq, Haskell among others. See the influence section above for the full list.
Is Lean self-hosting?
Yes, Lean is self-hosting — its compiler can compile itself.
When was Lean first released?
Lean was first released in 2013. It was designed by Leonardo de Moura.

Evidence Sources

Discover More

What are programming languages written in? Lean in the language family tree Interactive programming language graph Is Lean self-hosting? Compiler bootstrapping explained Languages that influenced Lean: Coq Languages that influenced Lean: Haskell
Explore Lean in Graph →