A newcomer to formalized mathematics today can easily receive a distorted picture of the field. Search for machine-checked proofs and Lean appears everywhere: in university courses, online communities, mathematical libraries, research on artificial intelligence, and ambitious projects to formalize modern mathematics. Lean deserves that attention. It combines a compact trusted core, a powerful elaborator and metaprogramming system, and a rapidly growing library.

But Lean arrived in a landscape already shaped by nearly half a century of experiments. Long before Lean, researchers had built systems around classical higher-order logic, constructive type theory, set theory, rewriting, induction heuristics, and generic logical frameworks. Some wanted a machine to verify textbook mathematics. Others wanted to prove hardware correct, synthesize programs from specifications, or automate the routine parts of mathematical argument. Their systems made different compromises because they were solving different problems.

Understanding that history changes how proof assistants look. They stop appearing as unusual text editors with elaborate type systems and start appearing as answers to four enduring questions:

1. What language should we use to state mathematics and computation?
2. Which part of the system must be trusted?
3. How much work should be done automatically, and how much should remain under human control?
4. What should a completed proof be: a script, a derivation, a program, or a certificate?

Key takeaway
“Proof assistant” names a family of architectures, not one technology. Lean is best understood as a modern synthesis of ideas that originated in several earlier traditions.

Before proof assistants: the dream and the obstacle

The dream of reducing reasoning to formal rules is much older than electronic computers. Mathematical logic in the nineteenth and early twentieth centuries made it possible to imagine proofs as symbolic objects that could, in principle, be checked step by step. Yet formalizing ordinary mathematics remained forbiddingly laborious. A paper proof suppresses thousands of small inferences: substitutions, type checks, uses of definitions, and appeals to previously known facts. A machine cannot safely treat these as “obvious” unless its software knows exactly what they mean.

Early automated theorem provers attacked a related but different problem: given a logical statement, could a program search for a proof? Search worked impressively in restricted settings, but it could also explode combinatorially. Interactive proof checking suggested another division of labor. A human would provide the structure of the argument; the machine would verify every formal step and automate only the parts for which reliable procedures were available.

That division became one of the field’s central ideas. It also raised a difficult engineering question: if a large program says that a theorem has been proved, why should anyone trust the program?

Automath: mathematics as a checkable document

In 1968, the Dutch mathematician N. G. de Bruijn began the Automath project. Its goal was unusually direct: create a language in which substantial pieces of mathematics could be written with enough precision for a computer to check them. De Bruijn presented Automath as a “language for mathematics,” not merely as a solver for isolated puzzles.¹

Automath introduced ideas that now feel strikingly modern. Definitions and proofs were represented in a typed formal language. The checker could remain comparatively small because it did not need to invent the proof; it only needed to verify the formal object supplied to it. Mathematical context—variables, assumptions, definitions, and dependencies—was made explicit.

This style of architecture later inspired what is often called the de Bruijn criterion: the final proof object should be checkable by a small, independently understandable kernel. The front end may be sophisticated, and proof search may be heuristic, but trust should concentrate in a narrow component.²

Automath did not become today’s dominant platform. Its notation was austere, computer interaction was primitive, and formal libraries were difficult to build and maintain. Its historical importance lies elsewhere. It demonstrated that a computer could check serious mathematics expressed in a type-theoretic language, and it established a pattern that would reappear in Rocq, Agda, Lean, and many certificate-checking systems.

Automath’s central intuition survives: complicated tools may help construct a proof, while a smaller component checks the resulting formal object.

LCF: making false theorems difficult to manufacture

A second foundational idea arose from work on Logic for Computable Functions, or LCF. Robin Milner and colleagues developed the Edinburgh LCF system during the 1970s as a framework for reasoning about programs and recursive functions. Its famous architectural move was different from Automath’s but closely related in spirit.³

In LCF, a theorem was represented inside the implementation language by a protected abstract data type. Ordinary programs could inspect a theorem or combine existing theorems, but they could not simply manufacture a value claiming that an arbitrary statement was true. Only a small set of trusted primitive inference functions could create new theorems.

This produced an elegant safety property:

A tactic may fail, loop, or choose an unhelpful proof strategy—but if it returns a theorem, that theorem must have been assembled through the trusted inference rules.

LCF also gave the field ML, originally the “metalanguage” used to program proof strategies.⁴ Tactics could be written as ordinary higher-order programs. This made proof automation extensible without enlarging the logical kernel every time a new search procedure was added.

The LCF architecture shifted the trust question. Instead of trusting every tactic, users primarily trusted the primitive theorem constructors and the language mechanisms that protected the theorem type. The idea became enormously influential. Modern proof assistants differ in implementation details, but many still separate a trusted kernel from a much larger layer of tactics, elaboration, simplification, and user interface code.

Common misconception: “A small kernel means the whole proof assistant is verified.”
It does not. A small kernel reduces the amount of code whose logical correctness is essential. Bugs elsewhere can still cause crashes, poor error messages, lost work, or misleading displays. The architectural claim is narrower: untrusted automation should not be able to make the kernel accept an invalid theorem.

From LCF to HOL: keep the logic stable, improve the tools

The HOL family grew directly from LCF. Michael Gordon adapted the LCF architecture to higher-order logic, a classical logic expressive enough to describe functions, predicates, sets, and mathematical structures in a uniform way. HOL88 and its descendants became important platforms for hardware and software verification. The 1993 book Introduction to HOL documented both the logic and the theorem-proving environment.⁵

HOL represents one durable philosophy of proof-assistant design:

• choose a comparatively small, well-understood classical logic;
• keep extensions conservative where possible;
• invest heavily in libraries and proof automation;
• use the LCF kernel discipline to protect soundness.

This is not a primitive or outdated design. A stable logic can be a major advantage in long-lived verification projects. It makes the semantic foundation easier to audit, and it encourages users to encode new mathematical structures within the logic rather than modifying the logic itself.

HOL’s success also shows why “expressive foundation” and “effective proof environment” are different dimensions. A system with a modest core language may support very sophisticated reasoning through definitions, derived rules, decision procedures, and libraries.

Isabelle: build a prover for logics, not just one logic

Lawrence Paulson’s Isabelle took another path. Rather than hard-code one object logic, Isabelle was designed as a generic theorem-proving framework. Its metalogic could represent the inference rules of different logics, allowing one proof infrastructure to host several foundations.⁶

This was an ambitious answer to a practical problem. Researchers repeatedly built theorem provers that shared the same mechanisms—unification, rewriting, simplification, proof search—but differed in their logical foundations. Isabelle asked whether those mechanisms could be made reusable.

The most widely used instance today is Isabelle/HOL, based on classical higher-order logic. Yet Isabelle’s architecture retains the historical idea that the proof assistant and the object logic need not be the same thing. Its libraries have hosted first-order logic, set theory, constructive type theory, and other systems alongside HOL.⁷

Isabelle also developed a distinctive style of readable, structured proof through the Isar language. This reflected another recurring concern in the history of proof assistants: a proof must not only convince the kernel; it must remain intelligible to humans who will maintain it years later.

The constructive branch: proofs that can behave like programs

A parallel tradition emerged from constructive logic and dependent type theory. Here the connection between proving and programming was not merely an implementation technique. It was built into the foundation.

Under the Curry–Howard correspondence, a proposition can be viewed as a type and a proof as a term inhabiting that type. A proof of an implication behaves like a function transforming evidence for the premise into evidence for the conclusion. A proof that an object exists can contain the object itself. Computation simplifies proof terms in much the same way that evaluation simplifies programs.

Thierry Coquand and Gérard Huet’s Calculus of Constructions, published in 1988, combined higher-order constructive logic with a powerful typed lambda calculus.⁸ It became the foundation of the Coq proof assistant, renamed The Rocq Prover with version 9.0 in March 2025.⁹

Rocq developed this foundation into the Calculus of Inductive Constructions, supporting inductive data, recursive functions, dependent types, and machine-checked proofs in one language. It also made program extraction a prominent use case: from suitably constructive definitions and proofs, the system can produce executable functional code.¹⁰

Other systems explored neighboring points in the design space:

• Nuprl emphasized constructive type theory and proof refinement, with a close relationship between proofs and extracted programs.
• Agda evolved into a dependently typed functional programming language that can also serve as a proof assistant. Its official description explicitly places it in the Martin-Löf type-theory tradition and stresses that constructive proofs can run as algorithms.¹¹
• Alf, Alfa, Epigram, and later languages such as Idris explored how dependent types could make verified programming feel more like ordinary programming.

This branch did not merely add a different syntax. It changed the meaning of equality, existence, and proof. It also created new tensions. A highly expressive dependent type theory can state remarkably precise specifications, but elaborating and checking those specifications is more complex. Computation inside the logic brings benefits, yet it requires careful rules to preserve consistency and decidable type checking.

The automation-first tradition: Boyer–Moore and ACL2

Not all proof assistants made interactive proof terms the center of the experience. Robert Boyer and J Strother Moore pursued a more automated style beginning in the 1970s, especially for reasoning about recursively defined functions. Their provers combined rewriting with heuristics for mathematical induction.

That lineage eventually produced ACL2, whose name expands to “A Computational Logic for Applicative Common Lisp.” ACL2 is at once a programming language, a first-order logic, and an automated theorem prover. Users model systems as executable Lisp-like functions and ask the prover to establish properties, often with considerable automation.¹²

ACL2’s history is a reminder that proof-assistant practice is not defined by dependent types or tactic scripts. For many engineering problems, a restricted executable logic plus strong domain-tuned automation is precisely the right choice. ACL2 has been used extensively for hardware and low-level systems verification, where predictable symbolic execution and induction can matter more than a maximally general foundation.

Mizar and the library-centered vision

The Mizar project, initiated by Andrzej Trybulec in 1973, pursued yet another goal: formal mathematics written in a style closer to ordinary mathematical prose and accumulated in a large shared library.¹³

Mizar’s importance is partly sociological. It treated a formal mathematical library not as a by-product but as a central scientific artifact. Definitions and theorems would be reusable, cross-referenced, and curated over decades. Today’s major libraries—Isabelle’s Archive of Formal Proofs, Rocq’s Mathematical Components and package ecosystem, Lean’s mathlib, and others—owe much to the recognition that the value of a proof assistant grows nonlinearly with the body of formal knowledge surrounding it.

A theorem prover without a library is like a programming language without a standard library: technically capable, but expensive to use. A library encodes not only results but conventions—how structures are represented, which abstractions are preferred, and how automation should find relevant facts.

PVS and integrated verification environments

The Prototype Verification System, or PVS, appeared in the early 1990s as an integrated environment for specification and verification. It combined a strongly typed classical higher-order logic with decision procedures and an interactive prover.¹⁴

PVS illustrates a recurring engineering strategy: enrich the specification language enough to catch mistakes early, then connect interactive proof with specialized automation. Predicate subtypes can express constraints in types; arithmetic solvers and simplifiers can discharge routine obligations; the user intervenes when semantic insight is required.

This architecture sits between simple logical kernels and domain-specific verification tools. It also anticipates a pattern common in modern systems: the proof assistant is less one algorithm than an orchestrated environment in which several reasoning methods cooperate.

Lean: a synthesis, not an endpoint

Lean was first described publicly as a new theorem prover in 2015. Its design combined a dependent type-theory kernel, an elaborator that could infer omitted details, programmable tactics, and an ambition to support both automated and interactive reasoning.¹⁵

Several historical lines meet in Lean:

• From Automath and constructive type theory comes the idea of proof terms checked by a small kernel.
• From LCF comes the separation between trusted inference and extensible proof automation.
• From ML-family systems comes the view of tactics and metaprograms as serious software.
• From Mizar and later library projects comes the recognition that a coherent mathematical library is an essential part of the platform.
• From systems such as Isabelle, HOL, Rocq, and PVS comes decades of experience in simplification, rewriting, automation, notation, and interactive environments.

Lean’s distinctive success is therefore not that it discovered mechanized proof from scratch. It packages mature ideas in a system whose engineering, language design, community, and library arrived at a favorable moment. Its current visibility should broaden curiosity about the field, not erase the systems that made it possible.

Different systems occupy different points in a multi-dimensional design space. There is no single axis from “weak” to “powerful.”

Why did the field not converge on one universal proof assistant?

Software markets often converge. Formal reasoning has resisted that pattern because foundational choices have consequences that are difficult to hide behind a common interface.

1. Different logics make different things easy

Classical higher-order logic is familiar, stable, and effective for a broad range of mathematics and verification. Constructive dependent type theory offers fine-grained specifications and a direct relationship between proof and computation. Set-theoretic foundations align with mainstream mathematical practice. First-order executable logics can support stronger automation.

Each choice creates both conveniences and obligations. There is no foundation that is simultaneously the simplest, most expressive, most computational, most automated, and easiest to implement.

2. Trust can be organized in several sound ways

A system may store explicit proof terms, use an LCF-style protected theorem type, reconstruct external solver results, check certificates, or trust verified decision procedures. These are not cosmetic differences. They determine the trusted computing base, proof-file size, replay performance, and how easily external automation can be connected.

3. Automation is domain-sensitive

A prover optimized for hardware bit vectors will not behave like one optimized for algebraic rewriting or dependent program synthesis. Some users want the system to search aggressively; others want precise control and predictable proof maintenance. The best balance depends on the problem.

4. Libraries create path dependence

Once thousands of definitions and theorems have been built around a representation, changing foundations is not like changing text editors. It is closer to porting an operating system. Mature libraries, community expertise, and integration with existing toolchains can matter more than abstract elegance.

5. Human factors are part of sound engineering

Proof language, editor feedback, error messages, refactoring tools, documentation, and teaching materials influence whether a system can support a long project. A logically elegant prover with an inaccessible workflow may be less useful than a theoretically modest one with excellent tools.

Key takeaway
Proof assistants coexist because they optimize different combinations of foundation, trust, automation, library design, and user experience. The plurality is evidence of a rich design space, not of a field that has failed to standardize.

A compact mental map

Tradition	Central idea	Representative systems	Natural strength
Proof-object checking	Represent proofs as typed formal objects checked by a small core	Automath, Rocq, Agda, Lean	Auditable trust and expressive formalization
LCF architecture	Protect theorem construction behind trusted primitive inferences	LCF, HOL, Isabelle	Extensible tactics without trusting each tactic
Generic logical frameworks	Reuse proof infrastructure across object logics	Isabelle	Multiple logics and reusable proof technology
Automation-first induction	Combine executable models, rewriting, and induction heuristics	Boyer–Moore provers, ACL2	Automated reasoning about recursive systems
Library-centered formal mathematics	Optimize readable formal texts and cumulative mathematical knowledge	Mizar and modern large libraries	Long-term reuse and mathematical scale
Integrated specification and proof	Combine expressive specifications with decision procedures and interaction	PVS	Engineering-oriented verification workflows

The categories overlap. Isabelle uses an LCF architecture. Rocq and Lean include extensive automation. HOL has large libraries. The table is not a taxonomy of mutually exclusive species; it is a map of the ideas that each lineage made especially visible.

The next chapter will also be plural

Proof assistants are now entering another period of rapid change. Better editors and language servers make interaction less opaque. Large formal libraries make automation more knowledgeable. External solvers can provide certificates or have their results reconstructed. Machine-learning systems can propose lemmas and proof steps, while kernels continue to decide whether those proposals are valid.

History suggests that these developments will not eliminate architectural diversity. They will make old questions more urgent. If an AI system proposes a proof, what checks it? If several solvers contribute evidence, how is that evidence composed? If a library spans millions of lines, how are definitions governed and refactored? If a system gains more powerful computation rules, what happens to type checking and trust?

Lean will be one important arena for those questions. So will Rocq, Isabelle, HOL, Agda, ACL2, PVS, Mizar, and systems not yet designed.

The most useful historical lesson is therefore not that one lineage won. It is that the field repeatedly advanced by discovering a new way to separate invention from checking, automation from trust, and mathematical meaning from software convenience. A modern proof assistant is the visible surface of those accumulated ideas.

Final takeaway
To look beyond Lean is not to diminish Lean. It is to see it more clearly: as one sophisticated member of a six-decade effort to make reasoning explicit, reusable, computational, and worthy of trust.

References