lean4-prover

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):

curl https://elan.lean-lang.org/install.sh -sSf | sh
# or on macOS:
brew install elan-init
elan default leanprover/lean4:stable

Basic Theorem Structure

-- Simple proposition proof
theorem my_first_theorem : 1 + 1 = 2 := by
  rfl

-- Implication
theorem modus_ponens (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by
  apply hpq
  exact hp

-- Universal quantifier
theorem add_comm_example : ∀ (a b : Nat), a + b = b + a := by
  intro a b
  omega

Core Tactics

-- intro: introduce hypotheses / universally quantified variables
-- apply: apply a function or lemma to the goal
-- exact: provide the exact proof term
-- rfl: reflexivity (proves a = a or definitional equalities)
-- simp: simplification using simp lemmas
-- ring: prove equalities in commutative rings
-- omega: decide linear arithmetic over Nat and Int
-- linarith: linear arithmetic reasoning with hypotheses
-- cases / rcases: case split on inductive types
-- induction: structural induction
-- constructor: prove a conjunction or existential
-- contradiction: close goal from contradictory hypotheses

-- Example combining tactics
theorem example_proof (n : Nat) (h : n > 0) : n + n > n := by
  linarith

theorem ring_example (a b : Int) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

Project Setup with Lakefile

# Create a new Lean 4 project
lake new my_project
cd my_project

# Project structure:
# my_project/
#   lakefile.lean      -- build config
#   lean-toolchain     -- Lean version
#   MyProject/
#     Basic.lean       -- source files