What is Lean?
Lean is a dependently typed theorem prover and functional programming language developed to formalize mathematics and verify correctness of proofs and software. Unlike typical programming languages, Lean treats code as a mathematical object — allowing statements to be proven rather than just executed.
It is widely used in mathematical research, logic education, and formal verification communities, especially after the rise of Lean 4.
Specs
Language Type: Dependently typed proof language + functional programming
Released: 2013 (continuously evolving)
Primary Use: Mathematics proof verification, logic, formal software reasoning
Execution Model: Interactive proof engine + compiler
Typing: Dependent types with proof irrelevance and strong inference
Example Code (Proof Equivalent of “Hello World”)
theorem hello : True := by
trivial
A more functional example:
def add (a b : Nat) : Nat := a + b
#eval add 3 4
How It Works
Lean programs are built from:
- Definitions (functions, types, theorems)
- Theorems with proofs
- Tactics (commands guiding the proof engine)
- Modules of mathematical structures and logic frameworks
Lean also includes:
| Feature | Purpose |
|---|---|
| Interactive proof mode | Helps build proofs step-by-step |
| Type inference | Reduces verbosity |
| Mathematical libraries | Large and growing ecosystem |
| Compiler in Lean 4 | Enables executable programs |
Lean 4 merges programming and theorem proving much more tightly than prior versions.
Strengths
- Strong ecosystem for mathematical formalization
- Assists theorem writing rather than manually constructing everything
- Actively used by universities and research groups
- Lean 4 allows real-world programming using formally verified logic
Weaknesses
- Very steep conceptual learning curve
- Best used by those with math or formal methods background
- Tooling still evolving in some areas
- Not intended for general-purpose development without verification context
Where to Run
Lean can be used with:
- VS Code + Lean extension (best experience)
- Online Lean interactive environments (Lean Web Editor)
- Command-line interpreter and REPL
- TIO.run (simplified environment)
Lean 4 requires a more modern toolchain than Lean 3.
Should You Learn It?
- For normal programming: Not necessary
- For formal verification, theorem proving, or advanced math: Absolutely
- For esolang exploration or language design study: Very interesting
- For building apps quickly: Not ideal
Summary
Lean combines programming and mathematics, enabling proofs that are machine-checkable and guaranteed correct. While niche and demanding, it represents a major tool in the growing field of verified computation — where correctness is not just expected, but proven.
Top comments (0)