Genealogy
Two thousand years of checked deduction.
Machine-checked proof was not invented in 2024 with AlphaProof, or in 2020 with GPT-f, or in 2013 with Lean. It was built over decades on a deductive substrate that runs back to Euclid. The table classifies what was already there, and what the AI wave changed.
Elements
The first surviving system of mathematics with proofs as derivations from explicitly stated axioms. The deductive form the entire later tradition extends — the substrate every prover ultimately re-enacts.
Begriffsschrift
A formula language for pure thought modeled on arithmetic. Predicate logic with quantifiers, axiomatic deduction, an explicit calculus rather than rhetorical proof. The recognizable ancestor of every modern proof assistant's underlying logic.
Entscheidungsproblem
Hilbert and Ackermann pose the decision problem for first-order logic. Gödel proves first-order completeness (1929) and the incompleteness theorems (1931) — fixing the upper bounds on what machine-checkable provability can be.
On computable numbers
Independent demonstrations that the Entscheidungsproblem is undecidable. The boundary of mechanical proof is fixed: not everything can be derived, but everything that can be derived can be checked.
List Processor
Programs as data, recursion, symbolic differentiation. LISP becomes the substrate on which the first generation of automated reasoning is written (resolution, unification, Boyer-Moore).
AUTOMATH
The first language designed for the computer-verification of mathematical proofs. Dependent types as the carrier of mathematical statements. The lineage every modern proof assistant traces.
An axiomatic basis for computer programming
Hoare logic: pre- and post-conditions, partial-correctness assertions, the inference rules that make program properties provable. The bridge from mathematical proof to software verification. CACM 12, 576–580.
Boyer–Moore · Mizar
The Boyer–Moore prover automates induction over recursive functions. Trybulec's Mizar establishes the long-running formal mathematical library and proof-checked journal. Two routes — automated and human-driven — both proven to work.
LCF
Edinburgh's Logic for Computable Functions. The trusted-kernel architecture is invented here: a small audited core, an unlimited tactic language layered on top. Every modern proof assistant — Lean, Coq, Isabelle, HOL — inherits this discipline.
HOL · Coq · Isabelle
The interactive theorem provers that the next four decades of formal verification run on. Higher-order logic (HOL); the Calculus of Constructions (Coq); a generic proof framework hosting many logics (Isabelle).
Kepler conjecture formalization begins
Hales's computer-assisted proof of the densest sphere packing — initially rejected by referees who could not check the computational part. The Flyspeck project (completed 2014) re-proves it in HOL Light and Isabelle, end-to-end machine-checked.
Z3 and the SMT era
Modern SMT (satisfiability modulo theories) makes large decidable fragments fast enough to be invoked as a sub-procedure by every higher-tier system. Z3 becomes the workhorse decision oracle behind Dafny, F⋆, and many Lean/Coq tactic backends.
seL4 and CompCert
A microkernel proven correct in Isabelle (seL4) and a C compiler proven correct in Coq (CompCert). The two existence proofs that "specification-level functional correctness for shipping software" is real, even if it costs person-years per ten thousand lines.
Lean 1 released
A dependently-typed proof assistant in the LCF lineage with an emphasis on metaprogramming and performance. Lean 4 (2021) makes the prover itself the host language; Mathlib (started 2017) becomes the largest open formal mathematical library.
GPT-f
The first language model to contribute proofs accepted into a formal library (Metamath). arXiv 2009.03393. The line that became expert iteration (Polu et al., arXiv 2202.01344, 2022) — generate, check, keep what verifies, retrain.
Mathlib4 and the Lean wave
Mathlib ports to Lean 4. Coverage broadens to include functional analysis, measure theory, and a substantial fraction of an undergraduate curriculum. The premise library that makes lemma-warm proving meaningfully cheaper.
AlphaProof · AlphaGeometry 2
IMO 2024 silver via Lean — AlphaZero-style RL with the kernel as reward oracle, ~80M autoformalized training statements, multi-day inference per problem. The first demonstration that the recipe scales to contest-grade goals at the cost of substantial compute.
Open-weight prover wave
DeepSeek-Prover-V2 (~89% miniF2F), Goedel-Prover-V2 (8B matches 671B-class), Kimina-Prover, Seed-Prover, Numina-Lean-Agent, Leanstral. The recipe — LLM + Lean + verifier-as-reward + autoformalized data + search — becomes commodity at the open-weight layer.
IMO 2025 · gold via natural language
Gold medals reached via long-form natural-language reasoning rather than Lean. The split between informal capability and formal guarantee becomes the central architectural question — and the case that hybrid systems (informal sketch + formal verifier) are the durable form.
Periodic Stack of Verification
A coordinate system for verified artifacts: ⟨S, V, E, D, C, R, τ⟩ — 115,200 cells. The Kepler-step relation E(x) ≥ θ(D) · μ(S, V). The stack is published; the cells fill as systems report their joules.
The reading
Two thousand years, one map.
Each era added a logic, a system, or a measurement that fills another cell on the table. The genealogy is the history of cells finding their coordinates.