A proof assistant is a software system that helps users construct and verify formal proofs. It represents definitions, assumptions, and claims in a precisely specified formal system and checks whether proposed arguments follow its inference rules. Used in mathematics and computer science, proof assistants combine human-directed reasoning with automation. Their applications include formalizing mathematical results and establishing properties of software, hardware, and programming languages. Unlike an informal mathematical proof, a machine-checked development must supply enough detail for every inference to be justified within the chosen foundations. (isabelle.in.tum.de)
Logical foundations
A proof assistant needs a formal language for statements and a calculus governing their derivation. Different systems adopt different foundations, including type theory, higher-order logic, and set theory. These choices affect how mathematical objects are represented, which principles are available, and how computation interacts with reasoning. Isabelle is a generic framework supporting several logics; its widely used Isabelle/HOL instance provides classical higher-order logic. (isabelle.in.tum.de)
In dependent-type systems such as Lean and Rocq, types may depend on values. Through the Curry–Howard correspondence, propositions can be represented as types and proofs as terms inhabiting those types. An implication corresponds to a function transforming evidence for its premise into evidence for its conclusion. Checking such a proof therefore involves checking that a term has the required type. Lean uses a dependent type theory derived from the Calculus of Constructions, while Rocq uses the Calculus of Inductive Constructions. (lean-lang.org)
Foundational principles must be distinguished from proved results. A theorem is established relative to definitions and assumptions, including any declared axioms. Acceptance by a checker does not independently establish that every assumption is appropriate or that the statement captures its intended informal meaning. (lean-lang.org)
Interactive proof construction
Users normally begin by defining objects and stating a target proposition. The interface displays a proof state containing local assumptions and outstanding goals. A proof step may solve a goal or replace it with simpler subgoals. For example, proving a conjunction requires establishing both components; proving an implication may introduce its premise as an assumption. (lean-lang.org)
A tactic is a procedure that performs proof-construction steps. Tactics can apply established theorems, rewrite expressions, simplify formulas, or conduct searches. Users combine them into scripts, while more structured proof languages can make the argument resemble mathematical exposition. Isabelle’s Isar language supports this structured style. Libraries of previously checked definitions and lemmas reduce the need to rebuild elementary mathematics for each project. (lean-lang.org)
The boundary between interactive and automated theorem proving is not absolute. Isabelle, for example, integrates external provers through Sledgehammer, which searches for useful facts and attempts to reconstruct proofs inside Isabelle. Automation assists with particular steps while the user can still supply the overall argument and intermediate claims. (isabelle.in.tum.de)
Kernels and trust
Many proof assistants separate elaborate proof-construction tools from a comparatively small kernel. In Lean and Rocq, tactics produce proof terms that the kernel checks. Ordinary errors in tactics need not compromise logical correctness: a malformed result should be rejected rather than accepted as a theorem. This separation allows proof automation to evolve without requiring every tactic implementation to be trusted. (lean-lang.org)
A related architecture originated in the LCF tradition. It restricts the creation of theorem values to primitive logical operations, allowing higher-level procedures to combine those operations without bypassing the inference rules. HOL systems inherit this approach. Edinburgh LCF, developed in the early 1970s, was an important predecessor of later interactive theorem provers. (cl.cam.ac.uk)
The trusted computing base nevertheless extends beyond an abstract logical calculus. Confidence depends on the checker’s implementation and the assumptions actually used. Some computational shortcuts additionally require trust in compilation or evaluation mechanisms. Independent checkers can reduce dependence on a single implementation, but they do not resolve mistakes in the formal statement itself. (lean-lang.org)
Representative systems
Lean combines a dependent-type theorem prover with a programming language and extensible proof automation. It supports mathematical formalization and software verification. Rocq, formerly called Coq, similarly combines dependent types, interactive proofs, and facilities for specifying and developing verified programs. (lean-lang.org)
Isabelle provides a general logical framework, structured proofs, and integrated automation. HOL Light concentrates on higher-order logic with a small logical core, programmable proof tools, and mathematical libraries. These systems differ in their foundations and interfaces; their theorem statements and proof artifacts cannot simply be treated as interchangeable. (isabelle.in.tum.de)
Applications and limitations
Mathematical applications include the formalization of the four color theorem in Rocq’s predecessor Coq. The Flyspeck project formalized the Kepler conjecture using HOL Light and Isabelle; the collaborative proof was completed in 2014. These developments checked substantial mathematical arguments and computational subclaims within explicit logical frameworks. (docs.rocq-prover.org)
In formal verification, proof assistants establish properties of computational systems against formal specifications. The CompCert compiler uses machine-checked reasoning to connect generated code with source-program behavior. HOL Light has also supported verification of floating-point arithmetic algorithms, including an exponential-function implementation whose error bound was formally established. (arxiv.org)
Formalization requires explicit definitions, supporting libraries, and detailed arguments. The resulting guarantee concerns the formal statement, not an unchecked paraphrase or every behavior of a surrounding physical system. Incorrect specifications, unsuitable assumptions, implementation faults in trusted components, and unfinished developments remain distinct sources of risk. Proof assistants make logical dependencies inspectable and mechanically checkable; evaluating whether those dependencies express the intended problem remains a separate task. (lean-lang.org)