Proof Assistants

Proof assistants — also called interactive theorem provers — are software systems that check mathematical proofs for correctness, step by step, with no reliance on human authority or intuition. Unlike automated theorem provers, which attempt to find proofs themselves, proof assistants require a human to write the proof and merely verify that each step follows from the axioms and previously established theorems according to the rules of a formal logic.

The major proof assistants include Coq, Isabelle, Lean, and Agda. Each implements a different logical foundation — Coq and Lean are based on dependent type theory; Isabelle on higher-order logic; Agda on Martin-Löf type theory — but they share a common architecture: a small, trusted kernel that checks proofs, and a larger, untrusted elaboration system that helps users construct them. The kernel is the critical component: it is small enough to be manually verified, and all trust flows through it.

Proof assistants have verified substantial bodies of mathematics: the four-color theorem, the Feit-Thompson theorem, the Kepler conjecture, and increasingly complex software systems. Vladimir Voevodsky championed them as the only way to ensure the reliability of modern mathematics, which has grown too complex for human verification. The field is moving toward proof assistants that can not only check proofs but suggest them, using machine learning to guide human mathematicians — a convergence that may reshape how mathematics is practiced within a generation.

Proof assistants are not a luxury for pedants; they are a necessity for a discipline that has outgrown the cognitive limits of its practitioners. The mathematician who refuses to use a proof assistant is like the pilot who refuses to use instruments — not a purist but a hazard.