Formal Methods: Machine-Verified Proof

Knowledge Map Atlas
Why Formalize? The Curry-Howard Correspondence Proof Assistants: A Landscape The 2026 Inflection: Machine Learning × Formal Methods

Why Formalize?

Readers of the discrete mathematics section have already met an unfinished story. In planar graphs, we proved the Five Color Theorem in roughly a page using Kempe chains, and then stated the Four Color Theorem with the brief note that its proof requires computer verification of a finite case analysis. We did not say what that means. We did not say whether such a proof can be trusted in the same sense as a hand-written one. We left the question open.

This page closes it. The answer is a thirty-year episode, beginning in 1976 and resolving in 2005, about what counts as a proof when computers are involved. It is also the story of the structural reorganization of mathematical trust that made the resolution possible.

From Hilbert to Gödel: certainty reorients

The goal of formalizing all of mathematics is older than computers. In the first decades of the twentieth century, David Hilbert articulated a program to codify the axioms and inference rules of mathematics so completely that every true mathematical statement could, in principle, be derived from them. The program also sought to prove the entire system's consistency by purely finite means. In this most ambitious form, the program sought certainty established by construction.

In 1931, Kurt Gödel proved that the goal, taken literally, is impossible. Any consistent formal system whose axioms can be listed by an algorithm, and which is strong enough to prove the basic facts of elementary arithmetic, contains true statements that cannot be derived within it. Such a system also cannot prove its own consistency by its own rules. The project was not abandoned, however. It was reoriented.

The new goal is more modest and, in retrospect, more useful: not absolute certainty, but a structured allocation of trust. Make explicit which parts of mathematical reasoning can be mechanically verified, which require human judgment, and where the boundary between them lies. Place the unavoidable acts of trust precisely, rather than scattering them invisibly throughout proofs.

The Four Color Crisis (1976-2005)

In 1976, Kenneth Appel and Wolfgang Haken announced a proof of the Four Color Theorem. The strategy was to reduce the question to a finite list of unavoidable configurations and verify the reducibility of each. The verification consumed roughly 1,200 hours of computer time on the machines of the era.

The mathematical community split. One camp accepted the proof. In its view, the logical reduction was rigorous, the verification mechanical and reproducible, and machines were arguably more reliable than human referees at checking thousands of cases without fatigue. Another camp rejected it. The philosopher Thomas Tymoczko, in a 1979 paper, argued that a proof a human cannot read in its entirety is not a proof at all. Paul Halmos echoed the sentiment more bluntly. The dispute was not about whether the theorem was true. It was about whether the means of establishing it counted as a proof.

The structural reason the dispute could not be settled is worth stating directly. The verification programs were written in IBM 370 assembly language, and later computer-assisted proofs likewise rested on programs written in conventional languages. To trust the proof, one had to trust those programs. To trust the programs, one had to inspect their source code by hand, which is exactly the activity the computer was supposed to replace. The chain of justification bottomed out in unverified imperative code, with no independent mechanism to break the regress. Disagreement could not be resolved because the parties were not pointing to a common, inspectable foundation.

The next two decades sustained the doubt. A 1981 independent check of part of the hand-verified portion of the argument found and corrected small errors in the original. The errors were not catastrophic, but they were enough to keep doubts about the whole argument alive. In 1996, a simpler proof by Robertson, Sanders, Seymour, and Thomas reduced the configuration count and tightened the argument, but the proof remained computer-assisted and the philosophical objection remained intact.

The resolution arrived in 2005. Georges Gonthier, working with the Coq proof assistant, reformulated the entire Four Color Theorem, logical core and configuration analysis alike, inside a single formal system whose verification procedure is a small, fixed, inspectable kernel program. Coq's kernel did the checking. The chain of justification became explicit. If one trusts the Coq kernel, the proof follows. Anyone who disagrees can now point to a specific object of disagreement, namely the kernel, and audit it. The thirty-year dispute did not end by consensus. It ended structurally, by clarification of where the residual trust resides.

The Pattern Recurs

Once stated, the pattern recurs across modern mathematics. Thomas Hales announced a proof of the Kepler conjecture in 1998. The Annals of Mathematics referees, after years of effort, were unable to declare full confidence in the proof's correctness. The admission was public and had no major precedent. Hales responded by launching the Flyspeck Project in 2003 to formalize the proof entirely in HOL Light and Isabelle. Eleven years later, in 2014, the formalization was complete and the Kepler conjecture passed from "almost certainly proven" to proven in the same sense the Four Color Theorem now is.

The 2020s have accelerated the trend. In December 2020, Peter Scholze publicly asked the Lean community to verify a key result in condensed mathematics, the so-called Liquid Tensor Experiment, because he was not personally certain his own proof was correct. A leading mathematician was asking a proof assistant for reassurance about his own work. The crucial lemma was formalized within about six months, and the full formalization was completed in 2022. In 2023, Terence Tao led a Lean formalization of the proof of the Polynomial Freiman-Ruzsa conjecture within weeks of the paper's publication. With that project, formal methods entered the active research workflow.

Remark: The Principle of Structured Trust

Formal methods do not deliver absolute certainty. The reorientation after Gödel was permanent, not a temporary retreat. What formal methods deliver is something more useful: a structured allocation of trust. Without that structure, debates about the correctness of a proof reduce to disputes about preferences, especially when the proof is long, computer-assisted, or machine-generated. With it, disagreements become specific. "Do you trust the kernel?" is a question that admits an answer. "Is this really a proof?" does not.

The Curry-Howard Correspondence

The Curry-Howard correspondence is not the name of a tool, a model, or a particular formal system. It is the name of a mathematical discovery: that logic and type theory are two surface presentations of the same underlying structure, with propositions matching types and proofs matching programs. The discovery is what licenses the architecture of Lean, Rocq, and every other modern dependent-type proof assistant. Understanding it is the entry point to understanding why such systems work.

The name

The correspondence carries two names because two logicians, working independently, found pieces of it at different times. Haskell Curry observed in 1934, and elaborated in 1958, that the type \(A \to B\) of functions from \(A\) to \(B\) obeys the same inference rules as the logical proposition "\(A\) implies \(B\)". The implication arrow and the function arrow are not analogous. They are the same arrow. Both the programming language Haskell and the technique of currying are named for Curry.

William Alvin Howard, in a 1969 manuscript circulated privately and published in 1980, extended Curry's observation into a systematic correspondence covering every logical connective. Conjunction, disjunction, negation, universal and existential quantification each acquired a type-theoretic counterpart, and the operations on proofs (modus ponens, case analysis, generalization) became the operations on programs (function application, pattern matching, binding).

Beginning in the early 1970s, Joachim Lambek added a third side. The same structure that appears in logic and in type theory also appears in category theory, where the relevant categorical structure (cartesian closed categories, in the simplest case) is a third equivalent presentation. The full three-way correspondence, Curry-Howard-Lambek, places logic, programming, and category theory as three faces of one mathematical object. We will encounter the categorical side later in the curriculum, on the page that defines cartesian closed categories.

Remark: Three Layers of Curry-Howard

The correspondence has substance at three depths.

The static layer identifies propositions with types. Each proposition corresponds to a type, and each type can be read as a proposition. The proposition "\(P\) and \(Q\)" is the product type \(P \times Q\), and the proposition "\(P\) implies \(Q\)" is the function type \(P \to Q\). This is the layer at which the correspondence is most easily stated.

The dynamic layer identifies proofs with programs. A specific proof of \(P \land Q\) is a specific pair \(\langle p, q \rangle\) consisting of a proof \(p\) of \(P\) and a proof \(q\) of \(Q\). A specific proof of \(P \to Q\) is a specific function that, given any proof of \(P\), produces a proof of \(Q\). Proofs are not described by programs. They are programs, in the same way that the number 3 is not described by the successor of 2 but is the successor of 2.

The operational layer identifies proof normalization with computation. Proofs can be simplified. A proof that constructs a pair and immediately projects out the first component can be reduced to a proof that uses the first component directly. Programs can be executed. The expression that constructs a pair and projects its first component evaluates to the first component. These are the same operation. In logic and in the lambda calculus, \(\beta\)-reduction is not two analogous procedures but one procedure viewed through two vocabularies. When a proof assistant checks a proof, it is type-checking a program, and whenever that check must compare two terms up to simplification, it carries out exactly this computation.

The correspondence in full

Theorem: The Curry-Howard Correspondence (Connective Table)

The standard logical connectives and their type-theoretic counterparts:

Logic Type theory
Proposition \(P\)Type \(P\)
\(P \land Q\)Product type \(P \times Q\)
\(P \lor Q\)Sum type \(P \oplus Q\)
\(P \to Q\)Function type \(P \to Q\)
\(\neg P\)\(P \to \bot\)
\(\forall x : X, P(x)\)Dependent function type \((x : X) \to P(x)\)
\(\exists x : X, P(x)\)Dependent pair type \((x : X) \times P(x)\)
\(\top\) (true)Unit type
\(\bot\) (false)Empty type

The two bold rows introduce the universal and existential quantifiers, which require a feature called dependent types, that is, types whose form depends on a value. To express "for every natural number \(n\), \(n + 0 = n\)", we need a type whose elements are functions taking an \(n\) and producing a proof of \(n + 0 = n\), where the proposition being proved changes with \(n\). Conventional programming languages cannot express such types. The dependent-type machinery is what gives proof assistants their full expressive power. The theorem proved on the following page quantifies over all real numbers \(x\) and \(y\), so its statement is a dependent function type of exactly this kind, although that page works with it through tactics rather than through the type theory directly.

Reframing the Boolean connectives, retroactively

A reader who has worked through Boolean Logic has already worked with every connective in the table above, in a different vocabulary. The truth table of \(P \land Q\) records its value. Given the values of \(P\) and \(Q\), it returns \(1\) if both are \(1\), and \(0\) otherwise. The Curry-Howard reading shifts focus from the value to the structure of the evidence. A proof of \(P \land Q\) consists of a proof of \(P\) together with a proof of \(Q\), that is, a pair.

The two readings are not the same statement. They live at different layers, one external (evaluation in a two-element set) and one internal (construction of evidence). What carries across is the syntax and the operational intuition, not the underlying logical system. The connectives \(\land, \lor, \to, \neg\) appearing in propositional logic and in the type theory of a proof assistant are formally distinct objects that share a notation.

Concretely, to construct a proof of \(P \land Q\), build a pair from a proof of \(P\) and a proof of \(Q\). To use a proof of \(P \land Q\), project out either component. The left projection gives a proof of \(P\), and the right projection gives a proof of \(Q\). The introduction and elimination rules of conjunction in natural deduction are, exactly, the constructor and projections of the product type. The same pattern holds for the other connectives:

A first look at the syntax

Lean is the proof assistant we will use to make these abstractions concrete. As a first taste, the proof that \(P \land Q\) implies \(P\) can be written in two equivalent ways. 


                    -- Term mode: the proof is written directly as an expression
                    theorem and_left (P Q : Prop) (h : P ∧ Q) : P := h.left

                    -- Tactic mode: the proof is constructed step by step
                    theorem and_left' (P Q : Prop) (h : P ∧ Q) : P := by
                      exact h.left

In both, the hypothesis h has type P ∧ Q, so it is a pair of a proof of P and a proof of Q. The expression h.left projects out the first component, yielding a proof of P. Term mode states this projection directly. Tactic mode wraps it in a by ... block that, in larger proofs, allows constructing the proof interactively, step by step. The two forms produce the same final proof object internally, and the choice between them is a matter of authoring style. The next section returns to this distinction.

Proof Assistants: A Landscape

The Curry-Howard correspondence is a mathematical observation. A proof assistant is a software system that implements it: a programming language whose type system is rich enough to encode mathematical propositions, together with the infrastructure to construct, check, and organize proofs as programs in that language. Several such systems exist. This section surveys the major ones and the architectural feature they share.

The major systems

Three proof assistants account for most contemporary work in formal mathematics:

The choice of system in any given project depends on the existing libraries, the surrounding community, and the foundational preferences of the authors. The mathematics being formalized is essentially the same in each. We will use Lean on the next page for its current research momentum, its large mathematical library, and the clean separation between its two proof-authoring modes.

Tactic mode and term mode, in practice

The two writing styles introduced at the end of the previous section deserve a closer look, because the distinction governs how mathematicians actually use these systems.

Term mode is the direct presentation, where the proof is written as a single expression of the appropriate type. It is concise, fits well in displayed equations, and matches most cleanly the Curry-Howard slogan that a proof of a proposition is a term of the corresponding type.

Tactic mode is the interactive presentation, in which the proof is constructed step by step inside a by ... block. At each step the system displays the current state of the proof, namely which hypotheses are available and what remains to be shown. The state is presented in a standardized format, with the available hypotheses listed first and the current goal on a final line marked by a turnstile. As a small example, suppose we wish to prove that if \(P \land Q\) holds, then \(Q \land P\) holds. 


                    example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
                      constructor
                      · exact h.right
                      · exact h.left

The constructor tactic decomposes a goal of the form \(Q \land P\) into two subgoals, one for \(Q\) and one for \(P\). This reflects the Curry-Howard reading that to construct a pair, one must construct each component. After constructor runs, the proof state shows: 


                    case left
                    P Q : Prop
                    h : P ∧ Q
                    ⊢ Q

                    case right
                    P Q : Prop
                    h : P ∧ Q
                    ⊢ P

The turnstile ⊢ marks the goal. The hypotheses are listed above it, and the goal follows it. The two cases are dispatched by the two lines beginning with ·, each producing the required proof from components of h. The experience is close to writing a proof on a blackboard, with the system tracking what has been established and what remains.

The two modes are extensionally equivalent. Internally, Lean executes tactics and produces a term-mode proof, which is then checked by the kernel. The kernel never sees tactics. This separation is the structural foundation of the trust architecture, which is the next subject.

The kernel and self-hosting trust

Every proof assistant has a kernel, a small program whose sole job is to check proofs. The kernel implements the rules of the underlying logic and nothing else: no automation, no tactics, no high-level convenience features. In Lean, the kernel is written in C++ and consists of several thousand lines of code. Rocq's kernel is similarly small. The smallness is deliberate, and the criterion below states the reason.

Definition: The de Bruijn Criterion

A proof assistant should produce proof terms verifiable by a small, independent kernel. The kernel is the only component whose correctness must be trusted by inspection. Every other component, including the elaborator, the tactic framework, and the library, need not be trusted, because whatever it produces is checked by the kernel.

The criterion is named after N.G. de Bruijn, whose 1968 Automath system was the first working proof checker built around this principle. Rocq and Lean follow the criterion directly. Isabelle belongs instead to the LCF tradition, which also confines trust to a small kernel but enforces it through a protected type of theorems rather than through proof terms that an independent checker can re-examine.

A notable feature of Lean's design is that almost everything above the kernel is itself written in Lean. This includes the elaborator that converts surface syntax into proof terms, the tactic framework, and mathlib. The system is largely self-hosting. This creates a trust loop with a useful property. The high-level machinery is itself a Lean program, and its correctness is, in principle, the sort of thing the kernel can verify. In practice, the high-level machinery is not exhaustively verified to date, but the architecture makes such verification possible in principle, with the kernel as the fixed point of the trust chain.

A fixed, inspectable point at the end of the trust chain is exactly the structural property that was missing from the Appel-Haken proof in 1976. Gonthier's 2005 Coq formalization made it explicit, replacing the unverified imperative code with a Coq proof checked by the kernel.

The Universal Pattern

The technique of attaching additional structured information to each primitive operation, and letting composition rules carry the information through automatically recurs across mathematics and computer science:

  • Automatic differentiation attaches derivatives to functions. The chain rule is the composition law.
  • Formal methods attach proofs of correctness to programs. Logical inference is the composition law.
  • Probabilistic programming attaches probability distributions. Conditional probability and marginalization are the composition laws.
  • Quantum computation attaches unitary evolution. Sequential and parallel composition of unitaries are the composition laws.

The four techniques are more than analogies. Each can be organized as a category whose morphisms carry the attached information and whose composition is the law named above. The language that names this structure is category theory, and we will return to it as a viewpoint of its own later in the curriculum. For now, the recognition that the same pattern recurs is the substantive observation.

Lean's boundaries

A clear-eyed account of any tool must say where the tool ends. Two boundaries circumscribe what a proof assistant does.

Verification is not discovery. Lean's primary function is to check proofs that are provided to it. Finding a proof in the first place is a separate problem, and the degree of automation depends on the domain. Some tactics close goals entirely on their own. The tactic rfl settles equalities that hold by definition, omega solves linear arithmetic over the integers, ring handles polynomial identities in commutative rings, and simp simplifies using a registered database of lemmas. Other tactics, such as aesop, search heuristically for a proof in a general goal-directed way. And learning-augmented tactics increasingly suggest or generate proofs in open-ended cases.

Yet three distinct ceilings limit proof discovery, and the popular discourse routinely conflates them. The first is logical. As Gödel's first incompleteness theorem (1931) shows, once a consistent system has axioms that an algorithm can enumerate and is strong enough for elementary arithmetic, some true propositions have no proof within it at all. The theorem is a statement about the gap between truth and provability, not about search. No algorithm, now or ever, can derive a proof that the system itself cannot produce.

The second ceiling is computability-theoretic. Even for propositions that are provable, whether a proof can be located by mechanical search depends on the decidability of the underlying problem. First-order logic's provability problem is semi-decidable. If a proposition is provable, an exhaustive search procedure will eventually find a proof. If it is not, the search may never terminate. Semi-decidability is a partial guarantee, not a limitation pulled from Gödel. It concerns the structure of algorithmic decision rather than the relation of truth to provability.

The third ceiling is complexity-theoretic. Even within domains where decision procedures exist and terminate, the practical limits of automated discovery are determined by the rate at which the search space grows. The same kind of considerations that underlie P vs NP apply here. In domains whose decision procedures perform well on the instances that arise in practice (quantifier-free linear arithmetic, polynomial identities, propositional logic), automation is routine, even though some of these problems, propositional satisfiability among them, are NP-complete in the worst case. Outside them, human strategy or learned heuristics drive the search. Most claims of the form "automation cannot achieve X" point to this ceiling, not to Gödel's.

Three Ceilings on Proof Search

The three ceilings are independent. Confusing them is the most common error in popular discussions of what proof assistants can and cannot do.

Ceiling Field What it actually says
Logical Logic (Gödel 1931) Some true propositions are not provable in the system at all. Not about search.
Computability Computability theory First-order provability is semi-decidable. Search finds proofs of provable statements but may not terminate on unprovable ones.
Complexity Complexity theory (P vs NP) Even decidable problems may be infeasible at scale. This is where practical automation limits actually live.

On an honest reading, most "automation cannot solve X" claims should cite combinatorial explosion or complexity-theoretic intractability, not Gödel. Gödel's theorem concerns propositions the system cannot prove at all, which rarely arise in everyday formalization, whereas complexity limits feasible search across the far larger class of propositions that are provable.

The system verifies what is written, not what was meant. Lean checks that a given proof establishes the proposition stated. Whether that proposition is the one the author intended to prove is a separate question, and one the system cannot answer.

A trivial example illustrates the point. The statement theorem length_nonneg {α : Type} (L : List α) : 0 ≥ 0 := by decide is true and admits a one-line proof, but if the author meant to assert that the length of a list is non-negative, the actual proposition being proved has nothing to do with lists. Lean accepts it. At most a style linter remarks that L is never used, and the checker itself has no way to detect the mismatch. This is the specification problem: the gap between intent and the formal statement of intent.

Remark: The Trust Pyramid

The trust structure of a formal development can be drawn as a pyramid. At the base sits the kernel, which is small, inspectable, and the only piece that must be trusted by direct audit. Above it sits the proof term, which the kernel checks mechanically. Above the proof sits the specification, the proposition being proved, which a human writes and a human must review. At the top sits the author's intent, which lives in cognition and cannot be formalized at all. Formal methods do not eliminate the top of the pyramid. They locate it precisely. Each layer's responsibility is explicit.

In practice, these gaps are mitigated through testable specifications, cross-checks, and design scrutiny. None of these measures eliminates the specification problem, but together they make it tractable.

These boundaries are not flaws to be lamented but the price of explicitness. Every formal system has them. What distinguishes formal methods is that the boundaries are visible. Each act of trust is located, and each unverified assumption is named. A system that promises "absolute correctness" hides its trust chain, whereas a system that promises "correctness relative to a stated specification" exposes it. The second promise is the one worth making.

The 2026 Inflection: Machine Learning × Formal Methods

The decade beginning around 2020 has been a period of rapid acceleration for formal methods, driven by two converging forces: the maturation of large mathematical libraries (chiefly mathlib) and the arrival of machine learning systems capable of generating proofs in the form a proof assistant can check. Together, these have produced a qualitative shift in what formal verification can accomplish at scale.

The Acceleration

The most visible developments since 2024:

  • In 2024, DeepMind's AlphaProof, working alongside a separate geometry system, achieved silver-medal-level performance on the International Mathematical Olympiad, with AlphaProof generating Lean-formal proofs of the problems it solved. This was the first widely-reported demonstration that a machine learning system could produce machine-checkable proofs at olympiad-mathematics level.
  • At IMO 2025, several machine learning systems reached gold-medal-level performance. The most publicized ones wrote their solutions in natural language, which human graders checked, while at least one, Harmonic's Aristotle, produced Lean proofs that the kernel verified directly.
  • By 2026, open-source machine learning proof agents had appeared under permissive licenses, bringing machine-assisted theorem proving into open use rather than keeping it inside proprietary systems.
  • A community effort known as CSLib, officially launched in early 2026, set out to formalize the core concepts of computer science in Lean, from models of computation to algorithms, and to build infrastructure for verifying real code. The effort extends the formal-mathematics project into computer science proper.

The cumulative effect is that the practice of formalizing mathematics, and of generating proofs by machine, is moving from a specialist research activity toward shared infrastructure for both mathematics and computer science, and mathlib has continued to grow at a rapid pace.

Why the trust structure makes this possible

Remark: The Trust Pyramid Under Machine Generation

The architecture of the trust pyramid, developed in the previous section, is exactly what licenses the pairing of machine learning with formal verification. When a machine learning system generates a proof:

  • The specification remains human-written and human-reviewed. The intent-to-specification gap, identified earlier as the irreducible top of the pyramid, is unaffected by the involvement of a learning system.
  • The proof is generated by the learning system and verified by the kernel. The generator may be unreliable, opaque, or stochastic, and the kernel does not care. If the proof passes verification, it is valid. If not, it is rejected and the generator tries again.
  • The kernel remains fixed and small, audited by humans on its own merits.

This division of labor matters because it dissolves an apparent contradiction. Machine learning systems are known to be unreliable at many tasks, while formal verification demands absolute reliability of the verified output. The two coexist because the verification step sits between them, mechanically converting "unreliable candidate proof" into either "verified theorem" or "rejected attempt". No middle ground exists. The learning system's fallibility is bounded by the kernel.