| Mission | |
| ======= | |
| Empower software developers to design, develop, and reason about programs. | |
| Empower mathematicians and scientists to design, develop, and reason about formal models. | |
| How | |
| --- | |
| Lean is an efficient functional programming language based on dependent type theory. | |
| It is under heavy development, but it already generates very efficient code. | |
| It also has a powerful meta-programming framework, extensible parser, and IDE support based on LSP. |