Pulled from a model and not double-checked. “Proof system” used broadly: formal logic, mechanized theorem proving, and cryptographic proofs of knowledge.

  • ~500bce panini, ashtadhyayi (formal generative grammar of sanskrit)
  • ~350bce aristotle, syllogistic logic + organon
  • ~300bce euclid’s elements (axiomatic geometry)
  • ~250bce archimedes, method of exhaustion (proto-limits)
  • ~263ce liu hui, commentary on the nine chapters (proofs in chinese math)
  • ~628 brahmagupta, brahmasphutasiddhanta (rules for zero / negatives)
  • ~820 al-khwarizmi, al-jabr (systematic derivation; gives us “algebra” and “algorithm”)
  • ~870 al-farabi, commentaries on aristotelian logic (organon transmitted + extended)
  • ~900 thabit ibn qurra, generalized pythagoras + early infinitesimal arguments
  • ~1020 ibn sina (avicenna), modal + temporal syllogistic, hypothetical syllogism
  • ~1070 omar khayyam, attempts on the parallel postulate; geometric solutions of cubics
  • ~1150 ibn rushd (averroes), aristotle commentaries that re-seed european logic
  • ~1250 al-tusi, further parallel-postulate work (precursor to non-euclidean geometry)
  • 1637 descartes, discourse on method / analytic geometry
  • 1666 leibniz, characteristica universalis (vision of a calculus of reasoning)
  • 1854 boole, laws of thought
  • 1879 frege, begriffsschrift (modern predicate logic)
  • 1889 peano axioms
  • 1900 hilbert’s 23 problems / hilbert’s program
  • 1910 whitehead & russell, principia mathematica
  • 1929 gödel completeness theorem
  • 1931 gödel incompleteness theorems
  • 1934 gentzen, natural deduction + sequent calculus
  • 1936 church-turing (lambda calculus, computability, undecidability of halting)
  • 1940 church, simple type theory
  • 1955 tarski, decision procedure for real closed fields
  • 1958 de bruijn, automath (early machine-checked math)
  • 1965 robinson, resolution (basis for prolog and SAT)
  • 1969 howard, curry-howard correspondence (proofs as programs)
  • 1971 cook, NP-completeness
  • 1972 martin-löf, intuitionistic type theory
  • 1976 four color theorem (appel-haken, first major computer-assisted proof)
  • 1983 boyer-moore (nqthm)
  • 1984 coq begins (coquand, huet — calculus of constructions)
  • 1985 GMR, interactive proofs and zero-knowledge (goldwasser, micali, rackoff)
  • 1986 fiat-shamir transform (interactive → non-interactive in ROM)
  • 1988 BGKW, multi-prover interactive proofs
  • 1989 IP = PSPACE (shamir)
  • 1989 isabelle (paulson)
  • 1992 PCP theorem (arora, lund, motwani, sudan, szegedy)
  • 1992 mizar mathematical library taking shape
  • 1994 kilian, succinct interactive arguments
  • 2000 micali, CS proofs (early SNARK precursor)
  • 2003 hales, kepler conjecture proof (later flyspeck’d in HOL/Isabelle)
  • 2005 four color theorem fully formalized in coq (gonthier)
  • 2006 zermelo-fraenkel-choice odd order theorem effort begins
  • 2008 lean 1 era ideas, z3 SMT solver (de moura, bjørner)
  • 2009 bitcoin (proof-of-work as economic proof system)
  • 2012 GGPR, quadratic arithmetic programs (basis for modern SNARKs)
  • 2012 odd order theorem formalized in coq
  • 2013 pinocchio (parno, howell, gentry, raykova) — first practical zk-SNARK
  • 2013 lean 1 (de moura, MSR)
  • 2014 zerocash → zcash (zk-SNARKs for private payments)
  • 2016 groth16 (most-deployed pairing SNARK)
  • 2017 bulletproofs (bünz et al, no trusted setup)
  • 2018 STARKs (ben-sasson, bentov, horesh, riabzev)
  • 2019 plonk (gabizon, williamson, ciobotaru) — universal updatable SRS
  • 2019 lean 4 announced
  • 2020 halo (BCMS) recursive proofs without trusted setup
  • 2020 nova, folding schemes for incrementally verifiable computation
  • 2021 liquid tensor experiment formalized in lean (scholze / commelin et al)
  • 2022 risc0 zkVM public release
  • 2023 fri-based STARKs in production (starknet, polygon zk)
  • 2023 plonky2/3, hyperplonk, lasso/jolt sumcheck-based zkVMs
  • 2024 sp1, jolt — general-purpose zkVMs for rust/RISC-V
  • 2025 broad mathlib coverage of undergrad math; growing AI-assisted lean proof search

Please let me know if there are any errors or obvious omissions.

upcoming?:

  • a major open problem solved with substantial machine assistance
  • LLM-driven proof autoformalization at scale
  • post-quantum SNARKs becoming the default
  • zkVMs fast enough for L1 execution
  • formally verified compilers + kernels in production-critical paths
  • AI training/inference attestations via SNARKs
  • a proof-of-correctness regime for safety-critical ML