Lean

Summary

Lean is a functional programming language and interactive theorem prover based on dependent type theory. It aims to bridge the gap between automated and interactive theorem proving, with applications in mathematical formalization and verified programming.

Paradigms

functional, purely functional, meta-programming

Domains

automated theorem proving, formal verification, education

Key Features

first-class functions, pattern matching, algebraic data types, type inference, meta-programming

Typing

dependent system, structural typing, strong typing, partial inference, compile-time checking, conservative type coercion, optional type annotations

Compilation

compiled

Influenced By

Coq, Agda, ML, Haskell, Idris, Isabelle

Ratings

File extensions

lean, hlean

External Links

• Lean official site
• Lean jobs at Devjobsscanner
• r/leanprover subreddit
• Trending GitHub repositories