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, …) inbymode. Ships Mathlib, ~1.6M lines of formalized math. - Prominent in AI mathematics: alphaproof (DeepMind, IMO silver-medalist), LeanDojo, miniF2F, ProofNet.
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