Proof Assistants: Foundations and Trust

Automatic proof search can be powerful while remaining unpredictable on difficult problems. A proof assistant allows people to organize the argument, introduce definitions, select lemmas, and delegate smaller tasks to automation.

Its central promise is that acceptance follows specified formal rules. Systems differ in the foundations they implement and in how their software enforces those rules.

The history should therefore follow several lineages. Treating every system as the same small kernel with a different interface obscures both mathematical and engineering choices.

Automath: a language for checking mathematics

N. G. de Bruijn began Automath in the late 1960s. The project investigated formal languages in which definitions and proofs could be recorded with enough precision for mechanical checking.

L. S. van Benthem Jutting's formalization of Landau's Grundlagen der Analysis, completed in the 1970s and documented in his 1977 thesis, demonstrated that the effort could encompass a substantial mathematical text.

The accomplishment involved more than verifying isolated formulas. A long development needs contexts, definitions, reusable results, and a disciplined account of how later expressions depend on earlier declarations.

Automath's significance includes its role in the history of dependent mathematical language. Its particular systems should nevertheless be distinguished from the later type theories and assistants that inherited related ideas.

LCF and the abstract theorem type

Robin Milner's Stanford LCF work in the early 1970s supported reasoning about computable functions. The Edinburgh LCF development, associated with Milner, Michael Gordon, Christopher Wadsworth, and collaborators, introduced an influential software architecture.

Its metalanguage, ML, provided an abstract type of theorems. Clients could manipulate theorem values but could construct them only through permitted primitive inference operations exposed by the trusted implementation.

A tactic could contain elaborate search code and still be unable to manufacture an arbitrary theorem value through ordinary well-typed client code. If a tactic failed, it should fail to construct the theorem rather than silently add an invalid inference.

This claim relies on the implementation language, abstraction boundary, and trusted operations behaving as intended. An abstract theorem value is not automatically an independently replayable proof object.

The 1979 Edinburgh LCF book documents a later stage than the initial Stanford system. The distinction matters when dating the architecture and ML's role.

HOL and Isabelle

Michael Gordon developed HOL in the 1980s to support reasoning about hardware using classical higher-order logic. HOL systems continued the LCF tradition while adopting a logical foundation different from dependent constructive type theory.

Lawrence Paulson's Isabelle provided a generic framework in which object logics could be represented within a logical infrastructure. Isabelle/HOL became a major application of that framework.

The generic framework and the chosen object logic are different levels. Saying that a theorem was proved “in Isabelle” leaves open which object logic and axioms were used.

Gordon's first-person history, “From LCF to HOL”, is valuable because it connects changes in logical representation to the verification tasks that motivated them.

Mizar and readable mathematical development

Andrzej Trybulec initiated Mizar in the 1970s. Its declarative language aimed to support mathematical texts whose organization remained recognizable to human readers.

The project developed a substantial library within a set-theoretic foundation. Types, registrations, and automated justification mechanisms help manage mathematical conventions and reduce repetitive detail.

This tradition emphasizes the relationship between formal precision and mathematical presentation. A readable surface still requires exact rules for interpreting omitted information and checking each inference.

Mizar also makes clear why the history of formalized mathematics must begin before the celebrated large verifications of the 2000s.

Induction and automated assistance

Robert Boyer and J Strother Moore developed an influential theorem-proving tradition centered on recursive functions, induction, rewriting, and carefully controlled automation.

Nqthm and later ACL2, developed with Matt Kaufmann and collaborators, made substantial contributions to reasoning about executable models and industrial verification.

These systems show that interactive theorem proving need not always resemble constructing explicit dependent proof terms. Users may guide automation through definitions, lemmas, and induction schemes.

Their trust arrangements must be assessed in their own terms. It would be inaccurate to describe every historical system as checking a complete proof object through an identical tiny kernel.

Dependent types and the Coq lineage

The Calculus of Constructions and its inductive extensions supported the development of Coq, associated with Coquand, Huet, Paulin-Mohring, and a large continuing group of contributors.

In this family, a proof can be represented as a term whose type is the proposition. Tactics help construct the term; the checker verifies that the resulting expression has the required type under the admitted definitions and axioms.

The project now uses the name Rocq. Historical accounts should retain “Coq” when identifying the system used in a dated publication or formalization.

Other dependent-type systems, including Nuprl, Agda, and later developments, explore different foundational and programming choices. Nuprl's computational type theory, associated with Robert Constable and collaborators, is an important reminder that dependent-type proof development has more than one lineage.

Metamath and minimal verification

Norman Megill introduced Metamath in the 1990s. Its framework checks formally specified substitutions and proof steps with a deliberately small collection of mechanisms.

A database supplies the axioms and inference patterns of the intended mathematics. The framework itself should be distinguished from a particular database, such as one developing set-theoretic mathematics.

Explicit proof data and independently implemented verifiers make replay and audit important parts of this approach. Smallness is an architectural advantage, but the correctness of the formal statement and the suitability of its axioms still require examination.

Lean and integrated elaboration

Leonardo de Moura and collaborators began Lean in the 2010s. Lean 4, developed with Sebastian Ullrich and others, integrates theorem proving with a substantial programming and elaboration framework.

Users write notation, omit inferable arguments, invoke tactics, and rely on libraries. Elaboration converts this surface language into explicit expressions suitable for the core type system.

The Lean reference manual describes the implemented theory. Claims about proof irrelevance, universes, choice, or equality should be checked against that particular specification rather than inferred from the general phrase “dependent types.”

A failed elaboration and a failed kernel check occur at different stages. Understanding the stages helps explain both the convenience of the interface and the source of formal assurance.

One theorem through three architectures

Take the elementary implication

In an LCF-style architecture, trusted inference operations construct a theorem for the assumed conjunction, derive its first conjunct, and discharge the assumption. Client code receives an abstract theorem value.

In a propositions-as-types presentation, a proof can be the term

The checker verifies the term's type using the rules for products and functions.

In a substitution-based proof framework, a proof record instantiates the database's relevant inference patterns, with the verifier checking substitutions, hypothesis references, and applicable variable restrictions.

The same elementary reasoning is represented differently. The comparison concerns architecture; it does not assert that every named assistant offers only one of these mechanisms.

Scripts, proofs, and trusted components

A proof script is a recipe for constructing or establishing a theorem within a system. It may depend on tactic names, search behavior, and library organization.

A proof object records evidence in a form that a checker can inspect. Some systems can export such evidence even when their ordinary interactive interface uses abstract theorem values or other internal representations.

The trusted components depend on the path used. External solvers may return certificates, have their arguments reconstructed, or be accepted through a more permissive oracle mechanism. Native computation can require additional trust compared with reduction inside the logical checker.

Imported axioms matter too. A theorem checked relative to an extra axiom is a theorem under that assumption. An unfinished placeholder accepted as an assumption does not disappear merely because the surrounding file compiles.

The useful question is therefore concrete: what statement was accepted, by which rules, under which assumptions, through which checking path?

Human direction remains mathematical work

Proof assistants reduce ambiguity in individual inferences. They also expose substantial choices about definitions, abstraction boundaries, intermediate lemmas, and library design.

Formalizing a proof can reveal a missing case or an unnoticed hypothesis. It can also require reorganizing a sound informal argument into a form more suitable for reusable formal development.

The broader history of interactive theorem proving documents these interacting mathematical and software traditions. No single system's chronology should stand in for the whole field.

The next two notes examine how formal reasoning applies to programs: first through deductive proofs, then through temporal models and algorithmic checking.

Sources and further reading

• N. G. de Bruijn, “The Mathematical Language AUTOMATH, Its Usage, and Some of Its Extensions” (1970).
• L. S. van Benthem Jutting, Checking Landau's Grundlagen in the AUTOMATH System (1977).
• Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth, Edinburgh LCF (1979).
• Michael J. C. Gordon, “From LCF to HOL: A Short History” (2000).
• Robert S. Boyer and J Strother Moore, A Computational Logic (1979); Boyer–Moore project history.
• John Harrison, Josef Urban, and Freek Wiedijk, “History of Interactive Theorem Proving” (2014).
• Leonardo de Moura and Sebastian Ullrich, “The Lean 4 Theorem Prover and Programming Language” (2021).
• Rocq project and Lean type-system reference, consulted for current terminology and implemented foundations.