A proof assistant (also called an interactive theorem prover) is software that helps construct and verify formal mathematical proofs. The user writes proof terms or tactics, and the system checks that each step follows from the rules of its underlying logic. If the proof type-checks, it is correct by construction.
Proof assistants implement the Curry-Howard correspondence: writing a proof is writing a program whose type encodes the proposition being proved. The type checker serves as the proof verifier.
Prominent proof assistants include:
- Lean — based on the Calculus of Inductive Constructions; emphasizes automation and a large mathematical library (Mathlib).
- Coq — one of the earliest mature proof assistants; uses dependent types and a tactic language.
- Agda — a dependently typed functional programming language with a focus on direct term construction rather than tactics.
- Isabelle — based on higher-order logic; provides a framework for defining logics and an extensive automation infrastructure.
Proof assistants have been used to verify substantial mathematical results (the four color theorem, the Kepler conjecture) and to certify software (the CompCert C compiler, the seL4 microkernel).
In this vault, formalization work targets Lean and Agda as the primary proof assistants. As the formal specifications of the semiotic universe and its extensions stabilize, they are candidates for mechanized verification.