A topic in the Open Knowledge Graph — a free, open map of 15,290 topics and the order to learn them in.
Interactive theorem proving uses software tools (proof assistants) in which humans construct formal proofs with machine verification of every step. The user states a theorem in a formal logic, then builds the proof interactively — applying tactics, introducing lemmas, and guiding the proof search — while the proof assistant checks that each step is logically valid. The result is a machine-checked proof: a certificate that the theorem follows from the axioms with absolute certainty. Major proof assistants include Coq (based on the Calculus of Inductive Constructions), Isabelle/HOL (based on higher-order logic), Lean (dependent type theory with strong automation), and Agda (dependently-typed programming language doubling as a proof assistant).
An informal mathematical proof convinces a human reader that a theorem is true. But human readers make mistakes — they may accept a flawed argument because it "looks right" or skip a tedious case analysis. Interactive theorem proving raises the bar: the proof must convince a computer, which checks every logical step mechanically against a fixed set of axioms and inference rules. The result is a machine-checked proof — a formal object that can be independently verified by anyone who trusts the proof assistant's kernel (typically a few thousand lines of code).
The workflow is fundamentally interactive. The user states a theorem in the proof assistant's formal language, producing a goal — a statement to be proved. The user then applies tactics (proof commands) that transform the goal into simpler subgoals. A tactic might split a conjunction into two subgoals, apply an induction principle, rewrite using a known equality, or invoke an automated decision procedure. Each tactic application is checked by the kernel: it must produce valid proof steps or be rejected. The process continues until all subgoals are discharged. The resulting proof term is a complete formal derivation, independent of the tactic scripts that generated it.
The major proof assistants differ in their foundational logics. Coq uses the Calculus of Inductive Constructions (CIC), a dependent type theory where propositions are types and proofs are programs — a direct implementation of the Curry-Howard correspondence. Isabelle/HOL uses classical higher-order logic, which is more familiar to working mathematicians and supports automation well (the Sledgehammer tactic calls external SMT solvers). Lean uses a dependent type theory similar to Coq's but emphasizes usability, metaprogramming, and strong automation; it has attracted significant mathematical formalization effort (Mathlib). Agda is a dependently-typed programming language where proofs are written as programs, emphasizing direct term construction over tactic-based proof.
The practical impact of interactive theorem proving has grown dramatically. CompCert (a verified C compiler in Coq) guarantees that compiled code faithfully reflects source semantics. seL4 (a verified microkernel in Isabelle/HOL) guarantees functional correctness and security properties of an operating system kernel. The Feit-Thompson Theorem and the Kepler Conjecture (Flyspeck project) have been formally verified, demonstrating that proof assistants can handle deep mathematics. The Four Color Theorem was verified in Coq, resolving concerns about the computer-assisted portions of the original proof.
The main barrier to broader adoption is the effort required to formalize proofs. Machine-checked proofs are typically 5-20 times longer than their informal counterparts because every implicit step, every appeal to "obviously," every routine calculation must be made explicit. This overhead is decreasing as automation improves — modern proof assistants can discharge many routine obligations automatically using SMT integration, rewriting engines, and proof search. The emerging pattern is human-guided, machine-verified development: the human provides the high-level proof strategy and key insights, automation handles the mechanical details, and the kernel guarantees correctness of the final result.