Lean 4 Theorem Prover

Formal theorem proving, mathematical verification, proof search, and type theory exploration.

When to Use / When NOT to Use

Use when: formal theorem proving, mathematical verification, proof search, type-theoretic reasoning, formalized mathematics with Mathlib, program verification.

NOT for: numerical computation (use scipy/numpy), symbolic algebra or calculus (use sympy), statistical analysis (use statsmodels), quick calculations.

Installation

If lean is not available, install via elan (the Lean version manager):