Interactive theorem proving

Interactive theorem proving (ITP) is the practice of constructing formal mathematical proofs with the assistance of a computer system, in which the human user provides the strategic insight and the machine verifies each logical step. Unlike fully automated theorem proving, which attempts to discover proofs without human guidance, ITP systems — also called proof assistants — are collaborative environments where the user directs the proof and the system enforces rigor. The interaction is typically conducted in a specialized formal language that combines mathematical notation with proof commands, or tactics, that instruct the system how to transform the current proof state.

The dominant systems in this tradition — Isabelle, Coq (now Rocq), Lean, Agda, and HOL Light — share a common architecture: a small, trusted kernel that checks the validity of each inference, and a larger, untrusted layer of automation that helps the user construct proofs efficiently. This separation is crucial. The kernel is small enough to be audited by hand; the automation can be as complex as necessary, because any mistake it makes will be caught by the kernel. The trust base is minimal, which is why these systems are used in safety-critical domains where a bug in the proof could mean a bug in the system being verified.

ITP has produced some of the most significant formalizations in modern mathematics: the four-color theorem (Gonthier, in Coq), the Kepler conjecture (Hales, in HOL Light and Isabelle), the odd-order theorem (Gonthier, in Coq), and increasingly large portions of algebraic geometry, number theory, and combinatorics in Lean's mathlib. These are not merely checks of known proofs; they are reconstructions that often reveal gaps, redundancies, and simplifications that human mathematicians had missed.

The philosophical significance of ITP is that it makes the social process of mathematical verification into a computational one. A proof in an ITP system is not an argument that convinces a referee; it is a data structure that compiles against a formal specification. This shifts the epistemic role of the mathematician from verifier to architect — from someone who checks steps to someone who designs the structures that the machine checks. Whether this is a gain or a loss depends on whether you believe that understanding a proof requires constructing it, or merely reading it.

The interactive theorem prover does not replace the mathematician; it replaces the mathematical community as the arbiter of correctness. This is a deeper change than it appears. A community can tolerate ambiguity, sketchiness, and appeal to intuition. A machine cannot. The question is whether the rigor of the machine clarifies mathematics or merely sanitizes it.