Lean 4 — where computation, types, and proof are welded together

Parent: logic

Lean 4 is a dependently-typed functional language and an interactive theorem prover — the working synthesis of this whole branch.

Foundation

The Calculus of Inductive Constructions (CIC): dependent type theory + inductive types (define ℕ, lists, trees, and propositions) + a universe hierarchy (Prop for proof-irrelevant propositions; Type u for data). Rich enough that a type can be any mathematical statement.

A proof is a term; checking = type-checking

By Curry–Howard, a proof of P is a term whose type is P. A small trusted kernel type-checks that term — the de Bruijn criterion: you only have to trust a tiny checker, not the whole system. Proof-checking = type-checking, in production.

Tactics — the human/machine bridge

You rarely write the proof term by hand. You run tactics (intro, apply, simp, ring, omega, …) that construct the term behind the scenes. Lean 4 is self-hosting: its tactic/metaprogramming language is Lean, so users extend the prover in the prover. This bridges human-style reasoning and the underlying normalized terms.

mathlib — formalized mathematics at scale

A massive, community-built library — analysis, algebra, topology, number theory — all machine-checked. It's the empirical proof that mathematics can be fully formalized, and the substrate for verified research (e.g. checking that a hard proof has no gaps).

The synthesis

Lean is a real, fast programming language and a prover, so verified programs and their proofs live in one object — programs = proofs literally. The three threads close here:

• computation (turing-machines, lambda-calculus) — Lean runs;
• types (type-theory) — Lean's foundation;
• proof (proof-theory) — Lean checks by normalization.

You write proofs the machine verifies by type-checking, and you can compute with them.