Lean (theorem prover)

An interactive proof assistant and programming language for writing and machine- checking formal mathematical proofs. Introduced to this wiki by lean-for-programmers.

What it is

• A proof assistant, not an automatic theorem prover: its kernel checks that expressions are well-formed and proof steps are legal; the IDE helps the user build proofs and suggests steps.
• Built on the Curry-Howard correspondence: propositions are types, proofs are terms of those types. Uses dependent types (types that depend on values) and universe levels to avoid paradoxes.
• Proofs are written with tactics (intro, cases, rw, simp, ring, omega, exact, …) in by mode. Ships Mathlib, ~1.6M lines of formalized math.
• Prominent in AI mathematics: alphaproof (DeepMind, IMO silver-medalist), LeanDojo, miniF2F, ProofNet.

New role, 2026-08-01 (ten-proofs). Lean stopped being only the place AI mathematics is done and became the place it is audited. OpenAI released a Lean 4.32.0 + mathlib formalization for each of ten claimed advances, so a reader checks the kernel instead of the press release. See lean-certificate.

Honest bridge to the knowledge-management cluster

The article’s history of mechanizing reasoning — Leibniz’s dream of a universal formal language plus a calculating machine, through Hilbert, Gödel, Church-Turing — overlaps directly with as-we-may-think: Bush (1945) also invoked Leibniz’s calculator and foresaw “a machine which will manipulate premises in accordance with formal logic.” Lean is, in a real sense, the realization of the mechanized formal reasoning that Bush gestured at, just as the memex anticipated the llm-wiki. The AI-proof angle (AlphaProof) also rhymes with the LLM-as-agent theme behind gbrain. These are genuine threads, not forced links — but Lean’s core domain (formal methods) remains distinct (cluster E).

Related

lean-for-programmers · as-we-may-think · ten-proofs · lean-certificate · alphaproof