34 Generative Models for Mathematics

Why Mathematics Matters for AI

What does it mean to understand a proof?

This question, deceptively simple, strikes at the heart of what separates genuine mathematical reasoning from mere symbol manipulation. A first-year undergraduate can verify that each line of a proof follows from the last, checking logical rules mechanically, yet walk away with no sense of why the theorem is true. A seasoned mathematician, reading the same proof, perceives the underlying architecture: the key insight that makes everything work, the places where the argument could break down, the generalisations that beckon from beyond the final QED. When we ask whether an AI system can “do mathematics,” we are really asking: which of these two experiences does it have? And does it matter?

The question matters because mathematics occupies a unique position in the landscape of cognitive tasks that AI aspires to perform. It is at once the most formal and the most creative domain of human thought. A mathematical proof, unlike an essay or a painting, admits an objective standard of correctness: either the argument is valid or it is not. Yet producing that proof requires intuition, pattern recognition, and the ability to see connections across distant areas of mathematics. It requires, in a word, insight.

The Appeal of Mathematics for Generative Models

Why should a researcher working on generative models care about mathematics? The answer lies in a problem that plagues nearly every application of generative AI: the evaluation problem.

Consider natural language generation. When a large language model writes an essay on the causes of World War I, how do we determine whether the output is “correct”? We might check for factual accuracy, logical coherence, stylistic quality, and argumentative persuasiveness, but each of these criteria is subjective, contested, and expensive to evaluate. Two expert historians might disagree on whether a particular claim is accurate. Two writing instructors might disagree on whether a particular paragraph is well-constructed. The very notion of “correctness” is slippery.

Now consider code generation. When a model generates a Python function to sort a list, we can test the output: run it on a battery of inputs and check whether the outputs match expectations. This is far better than natural language evaluation, and it is precisely this testability that has made code generation one of the most successful applications of large language models [55]. But testing has limits. A function that passes all tests might still be incorrect (the tests might not cover all edge cases), inefficient, or insecure.

Mathematics offers something even better than testing: proof. When a generative model produces a mathematical proof, the output can be checked with absolute certainty. Not approximately, not statistically, not “with high probability.” Absolutely. If the proof is formalised in a proof assistant such as Lean, Coq, or Isabelle, then a small, trusted kernel (typically a few thousand lines of code) can verify correctness in milliseconds. The proof is the evidence.

This observation has profound implications for training. In reinforcement learning from human feedback (RLHF) [56], the reward model is a proxy for human preferences, and misalignment between the proxy and the true objective is a constant worry. In mathematical reasoning, the reward is the proof checker itself: a binary signal (valid or invalid) that is never wrong and never needs calibration. This makes mathematics a uniquely clean training ground for developing general reasoning capabilities.

Mathematics is Harder Than Code

One might expect that the availability of perfect verification would make mathematical reasoning easier than code generation for AI systems. In practice, the opposite is true. As of 2025, the best language models solve approximately 70% of competition-level programming problems but fewer than 30% of competition-level mathematics problems at comparable difficulty levels [47]. Several factors explain this gap.

Flexibility of expression.

A correct Python function looks more or less the same regardless of who writes it. There are minor stylistic variations (variable names, choice of library functions), but the overall structure is largely determined by the specification. Mathematical proofs, by contrast, can look radically different while establishing the same result. Consider one of the oldest and most famous results in mathematics: the irrationality of $\sqrt{2}$.

We now present two entirely different proofs of Theorem 1, illustrating how the same mathematical truth can be established through fundamentally different lines of reasoning.

Both proofs are correct. Both establish the same result. But they employ different strategies, different intermediate lemmas, and different logical structures. The first proof is algorithmic: it follows a step-by-step descent argument. The second proof is structural: it leverages a deep property of the integers (unique factorisation) to derive a contradiction in a single stroke. A human mathematician recognises both as valid because they understand the meaning behind each step. A machine that processes proofs as token sequences must learn to recognise validity across these wildly different surface forms.

Natural language ambiguity.

Mathematical proofs, as they appear in textbooks and journals, are written in natural language interspersed with formal notation. This creates a profound difficulty for AI systems. Consider the phrase “it is obvious that.” To a human mathematician, this is a signal that the omitted steps are routine and can be filled in by the reader. To a machine, it is a gap in the logical chain that could hide anything from a trivial calculation to a subtle error.

Professional mathematics is full of such shortcuts. Authors write “by a standard compactness argument” without spelling out the argument. They write “WLOG” (without loss of generality) and expect the reader to verify that the claimed reduction is valid. They write “the proof is similar to Theorem 3.2” without specifying which parts carry over and which require modification. Each of these conventions makes proofs shorter and more readable for human experts, but creates obstacles for AI systems that must fill in every detail.

The verification gap.

The difficulty of natural language proofs creates what we call the verification gap: the distance between what a proof says and what a proof checker can verify. In code generation, this gap is small. A function written in Python can be executed directly; the language is its own verifier (via the interpreter and test suite). In mathematics, the gap is enormous. A proof written in English cannot be checked by any existing software without first being translated into a formal language, and this translation itself is a formidable AI challenge.

This gap has a direct consequence for training generative models. If we want to use proof correctness as a reward signal for reinforcement learning, we need proofs in a format that can be checked. This means either (a) training models to produce formal proofs directly, or (b) training models to translate informal proofs into formal ones. Both approaches have been pursued, and we will examine both in detail in subsequent sections.

Historical Context: The Dream of Mechanical Reasoning

The aspiration to mechanise mathematical reasoning is as old as mathematics itself. We survey the key milestones, not merely for historical interest, but because each milestone shaped the conceptual toolkit that modern AI for mathematics inherits.

Hilbert's programme.

In 1900, David Hilbert presented 23 unsolved problems that would shape the course of twentieth-century mathematics. His second problem asked whether the axioms of arithmetic are consistent, a question that reveals a deeper ambition: to place all of mathematics on a secure, mechanically verifiable foundation. Hilbert's programme aimed to (1) formalise all of mathematics in a complete axiomatic system, (2) prove that the system is consistent (free from contradictions), and (3) develop a decision procedure that could determine the truth or falsity of any statement within the system.

Had Hilbert's programme succeeded, the story of AI for mathematics would be very different. Mathematics would be decidable: every question would have a mechanical answer. The role of creativity and intuition would be, in principle, eliminable. There would be no need for generative models that “discover” proofs, because a brute-force search would suffice.

Gödel's incompleteness.

In 1931, Kurt Gödel shattered this dream with his two incompleteness theorems [41]. The first theorem states that any consistent formal system capable of expressing basic arithmetic contains statements that are true but unprovable within the system. The second theorem states that such a system cannot prove its own consistency. These results did not merely show that Hilbert's programme could not be completed in its original form; they established a fundamental limit on what formal systems can achieve.

The implications for AI are subtle and often misunderstood. Gödel's theorem does not mean that mathematical AI is impossible. It means that no single formal system can capture all mathematical truth, and that there will always be problems that require stepping outside the current framework to resolve. For practical purposes, the vast majority of mathematics that humans actually care about (analysis, algebra, geometry, number theory, combinatorics) can be formalised in standard foundations such as Zermelo-Fraenkel set theory with the axiom of choice (ZFC) or the calculus of inductive constructions used by Lean and Coq. The Gödelian limitations are real but remote: they concern statements at the frontier of mathematical logic, not the bread-and-butter theorems of working mathematicians.

Early automated reasoning.

The first automated theorem prover, the Logic Theorist, was created by Allen Newell and Herbert Simon in 1956 [57]. It proved 38 of the 52 theorems in Chapter 2 of Whitehead and Russell's Principia Mathematica, and for one theorem (2.85), it found a proof more elegant than the original. This early success fuelled enormous optimism. Simon famously predicted in 1958 that within ten years, a computer would prove a significant new mathematical theorem.

The prediction proved wildly optimistic. The combinatorial explosion of proof search, the difficulty of representing mathematical knowledge, and the brittleness of heuristic search strategies combined to ensure that automated theorem proving remained a niche endeavour for decades. Progress was steady but slow: resolution-based provers [22], tableaux methods, the development of SAT solvers, and eventually satisfiability modulo theories (SMT) solvers [26] expanded the class of problems that could be solved automatically, but always within narrow, well-defined logical fragments.

The four eras of mathematical AI.

We can roughly divide the history of AI for mathematics into four eras:

1. Symbolic era (1956–1990s): Hand-crafted heuristics, resolution provers, computer algebra systems. Success limited to narrow domains.

2. Statistical era (2000s–2010s): Machine learning applied to premise selection and proof guidance. Notable success with Vampire and E prover using learned heuristics [1].

3. Neural era (2017–2022): Deep learning for theorem proving. GPT-f [2], neural networks guiding Lean tactics. Proof of concept that language models can write proofs.

4. Generative era (2023–present): Large language models with reinforcement learning from proof verification feedback. AlphaProof [3], Lean Copilot, DeepSeek-Prover [4]. The era we are in now.

Each era built on the foundations laid by its predecessors, and the current generative era synthesises ideas from all three previous eras.

The key insight.

We arrive at the central observation that animates this entire chapter: formalization makes verification mechanical, and mechanical verification creates a perfect training signal for reinforcement learning. This insight connects the oldest dream in mathematical AI (Leibniz's calculus ratiocinator) to the newest techniques (RL with proof verification feedback). The dream of reducing reasoning to calculation has not been fully realised, but it has been partially realised in a form that Leibniz could not have anticipated: not as a universal decision procedure, but as a reward signal for training neural networks.

The social dimension.

There is another reason why mathematics matters for AI that is less often discussed: mathematics is fundamentally a social activity. Mathematicians do not work in isolation. They read each other's papers, attend each other's talks, build on each other's results, and occasionally disagree about whether a proof is correct. The history of mathematics is punctuated by famous errors: proofs that were accepted for years or decades before a flaw was found.

The Formalization of Mathematics

The idea of writing mathematics in a language so precise that a machine can check every step is both very old and very new. It is old because the dream of a universal formal language dates back to Leibniz and Frege. It is new because only in the last decade has formalization become practical enough to attract a critical mass of mathematicians, and only in the last few years has it become relevant to machine learning researchers.

In this section, we introduce the foundations of formal mathematics with an emphasis on the aspects that matter most for generative models: how mathematical statements are represented, how proofs are constructed and checked, and what kinds of mathematics have been formalised to date. The goal is not to turn the reader into a proof assistant expert, but to provide enough conceptual vocabulary to understand the AI systems that build on these foundations.

What Is Formalization?

Formalization is the process of translating mathematical statements and proofs from their natural, informal presentation (as found in textbooks, papers, and blackboard lectures) into a formal language that can be processed and checked by a computer. This process involves three key transformations:

1. Disambiguation. Every term must have a precise meaning. When a textbook says “let $f$ be a function,” the formalisation must specify: a function from what to what? Is it total or partial? Measurable? Continuous? The informal convention of leaving such details implicit must give way to explicit specification.

2. Completion. Every logical step must be justified. The phrase “it is easy to see that” must be replaced by an explicit chain of deductions. Every invocation of a theorem must be accompanied by a verification that its hypotheses are satisfied.

3. Encoding. The disambiguated, completed proof must be expressed in the syntax of a specific formal system. This involves choosing data structures for mathematical objects (natural numbers, real numbers, topological spaces), representing logical connectives and quantifiers, and organising the proof into a form that the proof checker can process.

The critical property of formal proofs is that checking is mechanical. Given a formal proof, a computer program (the proof checker or “kernel”) can verify its correctness by inspecting each step. This program is typically small (a few thousand lines of code), well-understood, and trusted. The entire edifice of formalised mathematics rests on the correctness of this kernel, and significant effort is devoted to keeping it simple and auditable.

A Brief History of Formal Verification Systems

The development of formal verification systems spans more than a century. We highlight the milestones most relevant to the story of AI for mathematics.

Principia Mathematica (1910–1913).

Alfred North Whitehead and Bertrand Russell's monumental Principia Mathematica [58] was the first serious attempt to derive all of mathematics from a small set of logical axioms. The work is heroic in scope and notoriously difficult to read. Its notation is impenetrable by modern standards. The proof that $1+1=2$ does not appear until page 379 of Volume I. Yet Principia established the principle that mathematics can be formalised, and that principle has never been overturned.

Automath (1968).

Nicolaas de Bruijn's Automath was the first computer language designed specifically for expressing mathematical proofs in a form that a computer could check [59]. Automath introduced several ideas that remain central to modern proof assistants: the use of type theory as a logical foundation, the representation of proofs as terms in a typed lambda calculus, and the principle that proof checking reduces to type checking.

Mizar (1973).

The Mizar system, created by Andrzej Trybulec, took a different approach: it aimed to make formalised mathematics as close as possible to the way mathematicians actually write [60]. Mizar proofs read almost like (very precise) English. The Mizar Mathematical Library, built over decades by the Mizar community, contains over 60,000 formalised theorems and represents one of the largest bodies of formalised mathematics in existence.

Coq (1984).

The Coq proof assistant, developed by Thierry Coquand and Gérard Huet at INRIA, is based on the Calculus of Inductive Constructions (CIC), a powerful type theory that can express virtually all of standard mathematics [61]. Coq introduced tactics: high-level proof commands that automate routine steps and allow the user to guide the proof at a strategic level. Notable achievements formalised in Coq include the four-colour theorem [62] and the Feit-Thompson odd-order theorem [63].

Isabelle/HOL (1986).

Lawrence Paulson's Isabelle is a generic proof assistant that supports multiple logical foundations, with Higher-Order Logic (HOL) being the most widely used [64]. Isabelle's “Sledgehammer” tool automatically calls external automated theorem provers (ATP) to discharge proof obligations, bridging the gap between interactive and automated theorem proving [65].

Lean (2013–present).

The Lean proof assistant, created by Leonardo de Moura at Microsoft Research and now developed as an open-source project, has become the most active venue for both mathematical formalisation and AI for mathematics [66]. Lean 4, the current version, is both a proof assistant and a general-purpose programming language, making it particularly well-suited for integration with machine learning systems. Its mathematical library, Mathlib [67], is the largest unified collection of formalised mathematics, containing over 100,000 theorems as of 2025.

A note on foundations.

The choice of logical foundation matters more than it might seem. Lean and Coq use type theory (specifically, variants of the Calculus of Inductive Constructions). Isabelle/HOL uses higher-order logic. Mizar uses set theory. These foundations are not identical in expressive power, though for practical purposes they can all express the same mathematics. The choice of foundation affects:

• Syntax: how theorems and proofs look on the screen.

• Automation: what the proof assistant can fill in automatically.

• Libraries: what has already been formalised and is available for reuse.

• Community: who is developing the system and what kinds of mathematics they prioritise.

For AI purposes, the choice of foundation translates directly into a choice of programming language for the generated proofs. A model trained to generate Lean proofs cannot generate Coq proofs without retraining, just as a model trained to generate Python code cannot generate Rust code. This fragmentation of the formal mathematics ecosystem is a significant practical challenge.

Type Theory and the Curry-Howard Correspondence

Most modern proof assistants (Lean, Coq, Agda) are based on type theory rather than set theory as their logical foundation. This choice, which may seem like a minor technical detail, has profound consequences for how proofs are represented and, consequently, for how generative models interact with formal mathematics.

The central idea is beautifully simple, and it is known as the Curry-Howard correspondence (or the “proofs-as-programs” interpretation). The correspondence establishes a deep analogy between two seemingly unrelated domains: logic and computation.

Let us unpack this with concrete examples.

Propositions as types.

Consider the logical proposition $A⟹B$ (“if $A$, then $B$”). Under the Curry-Howard correspondence, this proposition corresponds to the function type $A\to B$. A proof of $A⟹B$ is a function that takes a proof of $A$ as input and produces a proof of $B$ as output. This makes intuitive sense: if you can show me how to transform any evidence for $A$ into evidence for $B$, then you have shown that $A$ implies $B$.

Logical connectives as type constructors.

The correspondence extends to all logical connectives:

The last row is particularly elegant: the proposition “False” (a contradiction) corresponds to the empty type, which has no inhabitants. This means that a consistent logical system cannot prove “False,” just as a well-typed programming language cannot produce a term of the empty type.

The Calculus of Inductive Constructions

The logical foundation used by both Lean and Coq is the Calculus of Inductive Constructions (CIC), a dependent type theory that extends the Curry-Howard correspondence to handle the full richness of mathematical reasoning. We provide a high-level overview; the reader interested in formal details should consult Bertot and Castéran [61] or the Lean documentation [66].

Universes.

CIC organises types into a hierarchy of universes: $\text{𝙿𝚛𝚘𝚙}$, ${\text{𝚃𝚢𝚙𝚎}}_0$, ${\text{𝚃𝚢𝚙𝚎}}_1$, and so on. The universe $\text{𝙿𝚛𝚘𝚙}$ contains propositions (statements that are either true or false). The universe ${\text{𝚃𝚢𝚙𝚎}}_0$ contains ordinary types (natural numbers, lists, functions). Higher universes ${\text{𝚃𝚢𝚙𝚎}}_i$ contain types of types, enabling the construction of mathematical structures at arbitrary levels of abstraction.

Inductive types.

The “Inductive” in CIC refers to the ability to define new types by specifying their constructors: the ways in which elements of the type can be built. The natural numbers, for example, are defined by two constructors:

• $\text{𝚣𝚎𝚛𝚘}:\mathbb{N}$ (zero is a natural number), and

• $\text{𝚜𝚞𝚌𝚌}:\mathbb{N}\to \mathbb{N}$ (the successor of a natural number is a natural number).

Every natural number is either $\text{𝚣𝚎𝚛𝚘}$ or $\text{𝚜𝚞𝚌𝚌}(n)$ for some $n$, and this exhaustive case analysis is the foundation of proof by induction. More complex mathematical objects (lists, trees, groups, topological spaces) are defined as more elaborate inductive types.

Dependent types.

The key feature that makes CIC powerful enough for mathematics is dependent types: types that can depend on values. For example, the type $\text{𝚅𝚎𝚌𝚝𝚘𝚛}(n)$ of lists of length exactly $n$ depends on the natural number $n$. In a mathematical context, the type $\text{𝙸𝚜𝙿𝚛𝚒𝚖𝚎}(p)$ of proofs that $p$ is prime depends on the value of $p$. Dependent types allow the type system to express arbitrarily complex mathematical properties, and type checking enforces these properties automatically.

What Can Be Formalised?

A natural question is: how much of mathematics can actually be formalised? The answer is both encouraging and humbling.

In principle: virtually everything.

The standard foundations of mathematics (ZFC set theory, or equivalently the Calculus of Inductive Constructions) are powerful enough to express virtually all of the mathematics that humans have ever developed. Analysis, algebra, topology, number theory, combinatorics, probability theory, differential geometry: all can be (and to varying degrees have been) formalised in systems like Lean, Coq, and Isabelle.

In practice: a growing fraction.

As of 2025, the largest formalised library is Lean's Mathlib [67], which contains:

• Over 100,000 theorems and lemmas.

• Formalised coverage of undergraduate mathematics: linear algebra, group theory, ring theory, real and complex analysis, measure theory, topology.

• Significant graduate-level material: commutative algebra, algebraic geometry (schemes), category theory, representation theory.

• Notable individual achievements: the formalisation of Fermat's Last Theorem is underway (as a community project led by Kevin Buzzard at Imperial College London).

Yet Mathlib covers only a small fraction of the total body of known mathematics. The Mathematical Reviews database (MathSciNet) contains over 4 million reviews of mathematical papers. Even if each Mathlib theorem corresponds to several journal theorems, the gap is enormous. This gap is both a challenge and an opportunity for generative models: if AI can accelerate formalisation, the resulting formal libraries would be vastly more valuable as training data than the current collections.

What Cannot Be Formalised: Gödel's Shadow

We have established that virtually all of known mathematics can be formalised. But Gödel's incompleteness theorems (Theorem 4) tell us that no formal system can capture all mathematical truth. What are the implications for AI?

That said, the incompleteness theorems do have two important consequences for the design of AI systems:

1. No universal prover. There can be no AI system that proves all true mathematical statements, even in principle. Any prover must eventually encounter statements that are true but beyond its reach. This means that the “solve all of mathematics” goal is not merely practically difficult but logically impossible.

2. Foundation choice matters. Different formal systems can prove different sets of theorems. An AI system trained on proofs in one foundation might not transfer to another. The choice of formal system is a design decision with real consequences.

Mathlib: A Case Study in Large-Scale Formalisation

No discussion of formalization in the context of AI would be complete without a detailed look at Mathlib, the mathematical library for Lean. Mathlib is not merely a collection of theorems; it is a dataset, and understanding its structure is essential for understanding how generative models are trained on formal mathematics.

Scale and scope.

As of early 2025, Mathlib contains approximately:

• 100,000+ formalised definitions and theorems.

• 1.5 million lines of Lean code.

• Coverage of 30+ branches of mathematics.

• Contributions from 400+ mathematicians and computer scientists worldwide.

The library is organised hierarchically. At the foundation lie basic type theory, logic, and natural number arithmetic. Above this sit the algebraic hierarchy (monoids, groups, rings, fields, modules, algebras), the topological hierarchy (topological spaces, metric spaces, uniform spaces, compact spaces), and the analytical hierarchy (limits, continuity, differentiation, integration, measure theory). Each layer builds on those below, and the dependency graph is both deep and wide.

As a training dataset.

From the perspective of generative AI, Mathlib offers several advantages as a training dataset:

1. Ground truth. Every theorem in Mathlib has been verified by Lean's kernel. There are no errors, no gaps, no hand-waving. This makes it a uniquely clean dataset compared to, say, mathematics scraped from the internet.

2. Structured metadata. Each theorem has a name, a precise statement, a proof, a list of dependencies, and a position in the import hierarchy. This metadata supports a variety of learning tasks: next-theorem prediction, proof synthesis, premise selection, and more.

3. Diverse proof strategies. Mathlib proofs range from one-line tactic invocations (“simp”) to multi-hundred-line constructions involving dozens of intermediate lemmas. This diversity provides training signal at multiple scales.

4. Living codebase. Mathlib is actively developed, with new theorems added daily. This creates a natural evaluation methodology: can a model prove theorems that were added after its training data was collected?

The Landscape of AI for Mathematics

Having established the foundations of mathematical formalization, we now survey the landscape of AI approaches to mathematical reasoning. This landscape is rich and rapidly evolving, with roots in classical automated theorem proving, branches extending through modern deep learning, and new shoots emerging from the intersection of large language models and formal verification.

Understanding this landscape is essential for appreciating the generative models that are the focus of the remainder of this chapter. Each approach brings distinct strengths, and the most powerful modern systems combine ideas from multiple traditions.

A Taxonomy of Approaches

We organise the space of AI for mathematics into four broad categories, each defined by its relationship to formal and informal mathematical language:

1. Symbolic Automated Theorem Proving (ATP). Systems that operate entirely within formal logic, using search and inference rules to derive proofs. Examples include resolution provers (Vampire, E), tableaux provers, and SAT/SMT solvers (Z3, CVC5).

2. Neural Theorem Proving (NTP). Systems that use neural networks to guide proof search within a formal proof assistant. The neural network suggests tactics or proof steps, and the proof assistant verifies each step. Examples include GPT-f [2], PACT [8], and ReProver [9].

3. LLM-Based Mathematical Reasoning. Systems that use large language models to reason about mathematics in natural language, without necessarily producing formal proofs. Examples include Minerva [10], chain-of-thought reasoning [11], and tool-augmented approaches.

4. Hybrid Neuro-Symbolic Approaches. Systems that combine neural language models with formal verification, typically through autoformalization (translating informal mathematics to formal proofs). Examples include AlphaProof [3], DeepSeek-Prover [4], and Lean Copilot.

The Pre-Generative Era: Symbolic Methods

Before neural networks entered the picture, automated theorem proving was a purely symbolic enterprise. The fundamental idea is simple in principle: given a set of axioms and a goal, systematically search the space of possible derivations until a proof is found. In practice, the search space is astronomically large, and the art of ATP lies in finding good strategies to prune it.

Resolution.

The most influential technique in classical ATP is resolution, introduced by Alan Robinson in 1965 [22]. Resolution works in first-order logic with clausal form. Every formula is converted to a set of clauses (disjunctions of literals), and the resolution rule derives new clauses from existing ones by identifying complementary literals. If the empty clause is derived, the original formula set is unsatisfiable, which (by refutation) proves the desired theorem.

Resolution is complete for first-order logic: if a theorem is true, resolution will eventually find a proof. But “eventually” can mean “after the heat death of the universe.” The practical success of resolution provers like Vampire [68] and E [69] depends on sophisticated heuristics for selecting which clauses to resolve, which substitutions to try, and which derived clauses to retain.

SAT and SMT solvers.

The Boolean satisfiability problem (SAT) asks whether there exists an assignment of truth values that satisfies a given propositional formula. Despite being NP-complete, modern SAT solvers can handle instances with millions of variables, thanks to techniques like conflict-driven clause learning (CDCL). Satisfiability Modulo Theories (SMT) extends SAT with background theories (arithmetic, arrays, bit vectors), enabling reasoning about richer domains [26].

SAT/SMT solvers have proven remarkably effective for certain mathematical problems, particularly in combinatorics. Notable examples include the resolution of the Boolean Pythagorean triples problem by Heule, Kullmann, and Marek [70], which produced a proof of 200 terabytes, the largest proof ever generated at the time.

Strengths and limitations.

Symbolic ATP methods have two great strengths: they produce verified proofs (every step is logically justified), and they can handle problems with deep combinatorial structure. Their main weakness is that they lack mathematical intuition: they cannot read a theorem statement and “see” the right proof strategy. They explore the search space blindly, guided only by syntactic heuristics. This makes them excellent at proving lemmas that require mechanical bookkeeping but poor at proving theorems that require creative insight.

The Neural Revolution: Learning to Prove

The entry of neural networks into theorem proving marked a qualitative shift. Instead of relying on hand-crafted heuristics, neural systems learn proof strategies from data. The key insight is that a neural network can be trained to predict which proof step (tactic, lemma, or transformation) is most likely to make progress, given the current proof state.

Premise selection.

The earliest applications of machine learning to theorem proving focused on premise selection: given a conjecture to prove, which lemmas and definitions from the library are most likely to be useful? This is a classification problem: for each potential premise, predict whether it will appear in the proof. Early work by Urban [1] and Kaliszyk [71] showed that even simple machine learning models (k-nearest neighbours, naive Bayes) could significantly outperform hand-crafted heuristics at this task.

GPT-f and the language model approach.

The paper that launched the neural theorem proving era was GPT-f by Polu and Sutskever [2], which demonstrated that a GPT-style language model, fine-tuned on Lean proofs, could generate valid proof steps. The approach is conceptually simple: the model takes the current proof state (the goals and hypotheses) as input and generates the next tactic as output. If the generated tactic is accepted by the proof assistant, the proof state advances; otherwise, the model tries again.

GPT-f proved 56.5% of test theorems from a Lean benchmark, outperforming the previous state of the art. More importantly, it found 23 new proofs of theorems in Mathlib that had been manually proved by human mathematicians, several of which were shorter than the original proofs. This demonstrated that language models could not merely imitate human proofs but occasionally improve upon them.

PACT and expert iteration.

Han et al. introduced PACT (Proof Artifact Co-Training), which interleaves proof search with model training [8]. The model generates proofs, the successful proofs are added to the training set, and the model is retrained on the expanded dataset. This expert iteration loop (also known as “self-play for theorem proving”) allows the model to bootstrap from a small initial dataset of human proofs to a much larger dataset of machine-generated proofs.

ReProver and LeanDojo.

Yang et al. developed LeanDojo, a framework for extracting training data from Lean and interacting with the proof assistant programmatically, along with ReProver, a retrieval-augmented neural theorem prover [9]. ReProver uses a retrieval module to select relevant premises from Mathlib before generating tactics, addressing a key bottleneck: the vast size of the library makes it impossible for the model to “memorize” all relevant lemmas.

LLMs Enter the Arena

The release of GPT-4 [72] and subsequent large language models marked a new era for mathematical AI. These models, trained on vast corpora of internet text (including mathematical textbooks, papers, and forum discussions), demonstrated an unexpected capacity for mathematical reasoning without any specialized training on formal mathematics.

Chain-of-thought reasoning.

Wei et al. [11] showed that prompting a language model to “think step by step” dramatically improves its performance on mathematical word problems. Instead of jumping directly from problem to answer, the model generates a sequence of intermediate reasoning steps, each building on the last. This chain-of-thought approach does not guarantee correctness (the reasoning can still be flawed), but it provides a scaffold that makes errors easier to detect and correct.

Minerva and mathematical specialisation.

Google's Minerva [10] fine-tuned a large language model on a curated dataset of mathematical text, including textbooks, papers, and web content with mathematical notation. Minerva achieved state-of-the-art performance on several mathematical benchmarks, including MATH (a dataset of competition-level problems) and GSM8K (a dataset of grade-school math problems), without using any formal proof assistant.

The gap between informal and formal.

The remarkable success of LLMs on informal mathematical reasoning comes with an important caveat: the outputs are not verified. An LLM can produce a fluent, plausible-looking proof that contains subtle logical errors. It can invoke theorems that do not exist (“hallucinated” lemmas). It can skip steps that seem obvious but are actually wrong. Without formal verification, there is no reliable way to distinguish a correct proof from a convincing fake.

This limitation is not merely theoretical. Studies have shown that LLMs produce mathematical errors at significant rates [73], including errors that are difficult for human reviewers to detect. The errors tend to cluster at “hard” steps where genuine mathematical insight is required, precisely the steps where AI assistance would be most valuable.

Mathematical olympiad performance.

The most dramatic demonstration of LLM mathematical capabilities has come from competition mathematics. The International Mathematical Olympiad (IMO) has served as a high-profile benchmark. While pure LLM-based approaches (without formal verification) have shown impressive results on simpler competition problems, they struggle with the multi-step reasoning required by IMO-level problems. This performance gap has driven the field toward hybrid approaches that combine the intuition of LLMs with the rigour of formal verification.

The Key Insight: Autoformalization

The previous subsections revealed a tension. Symbolic ATP systems produce verified proofs but lack mathematical intuition. LLMs possess mathematical intuition but produce unverified output. Neural theorem provers bridge this gap by using neural networks to guide formal proof search, but they are limited by the availability of formal training data.

Autoformalization resolves this tension by using language models to translate informal mathematics (written in natural language with mathematical notation) into formal mathematics (written in Lean, Coq, or Isabelle). The idea is to leverage the vast quantities of informal mathematical text available on the internet and in textbooks, while using formal proof assistants to verify the results.

The significance of autoformalization for generative models cannot be overstated. It creates a data flywheel: informal mathematics (abundant but unverified) is translated to formal mathematics (scarce but verified), which produces new training data for both the translation model and the proof generation model. Each turn of the wheel increases the pool of formal mathematics available for training, which in turn improves the models, which in turn enables more formalisation.

Early work.

The idea of autoformalization was articulated by Szegedy in 2020 [74], who argued that autoformalization could be the “Rosetta Stone” connecting the vast informal mathematical literature to formal proof assistants. Wu et al. [75] demonstrated that large language models could translate informal mathematical statements into formal Isabelle code with surprising accuracy, even without fine-tuning on paired informal-formal data.

The role of verification.

What makes autoformalization particularly powerful is that the translations can be verified. If the LLM translates an informal theorem into a formal statement and the formal statement type-checks in Lean, we know the translation is at least syntactically valid. If the LLM also provides a proof and the proof is accepted by the kernel, we know the formal statement is true (in the formal system). The remaining question is whether the formal statement faithfully captures the intent of the informal statement, and this is the primary source of error in autoformalization.

Reinforcement Learning with Proof Verification

The final piece of the modern mathematical AI puzzle is the use of reinforcement learning (RL) to train models that generate proofs, using the proof assistant as the reward signal. This approach combines the pattern recognition capabilities of neural networks with the rigorous checking capabilities of formal systems.

The setup is natural:

• State: the current proof state (goals and hypotheses) in the proof assistant.

• Action: a tactic or proof step generated by the model.

• Reward: $+1$ if the proof is completed (all goals discharged), $0$ otherwise (with optional intermediate rewards for making progress).

• Environment: the proof assistant itself, which deterministically updates the proof state in response to each action.

This formulation has several attractive properties. The environment is deterministic: the same tactic always produces the same state transition. The reward is binary and reliable: either the proof compiles or it does not. The state is fully observable: the proof assistant displays all current goals and available hypotheses. These properties make theorem proving a “clean” RL environment, free from the noise and partial observability that complicate many other RL applications.

AlphaProof.

In 2024, DeepMind's AlphaProof system [3] demonstrated the power of this approach by solving four of six problems from the International Mathematical Olympiad (IMO), achieving a score that would have earned a silver medal. AlphaProof combined a language model (for translating competition problems into formal statements) with a reinforcement learning system (for searching for formal proofs in Lean). The system was trained through millions of iterations of self-play, generating proof attempts, verifying them, and using the results to improve the model.

DeepSeek-Prover.

Xin et al. [4] developed DeepSeek-Prover, which uses a large language model fine-tuned on Lean proofs with RL from proof verification feedback. The key innovation is the use of whole-proof generation: instead of generating one tactic at a time (as in GPT-f), DeepSeek-Prover generates entire proofs in a single pass, relying on the Lean compiler to verify the result. This approach is simpler and more scalable than step-by-step search, at the cost of requiring the model to plan the entire proof structure in advance.

Comparison with Code Generation

Throughout this section, we have drawn comparisons between mathematical reasoning and code generation. It is worth making these comparisons explicit, as the similarities and differences illuminate the unique challenges and opportunities of AI for mathematics.

The most striking difference is the data asymmetry. GitHub contains billions of source files in dozens of programming languages. Mathlib contains 100,000 theorems in a single proof assistant. This three-to-four order-of-magnitude gap in training data is the single biggest obstacle to applying the techniques that succeeded in code generation (large-scale pretraining on source code) to theorem proving.

The second major difference is the verification quality. Code generation uses tests, which are incomplete: a function can pass all tests and still be wrong. Theorem proving uses formal verification, which is complete: a proof that type-checks is guaranteed to be correct (modulo the consistency of the underlying foundations, which is universally assumed). This higher-quality verification signal is both a blessing (it enables cleaner RL training) and a curse (it sets a higher bar for the model to clear).

Preview: The Road Ahead

Having surveyed the landscape, we now have the conceptual vocabulary needed to understand the specific systems and techniques that will be explored in the remainder of this chapter. The road ahead covers the following territory:

1. Neural theorem proving in depth: how models represent proof states, generate tactics, and search the proof tree.

2. Autoformalization: translating between informal and formal mathematics using language models, with a focus on training data creation and evaluation.

3. RL for mathematics: the specific RL algorithms, reward structures, and training curricula used to develop mathematical reasoning capabilities.

4. Evaluation and benchmarks: how we measure progress in AI for mathematics, from simple competition problems to research-level conjectures.

5. Open problems: the frontier challenges that remain, including reasoning about novel mathematical structures, generating readable proofs, and approaching research-level mathematics.

Each of these topics builds on the foundations laid in this section: the formalization of mathematics provides the language, the taxonomy of approaches provides the conceptual framework, and the RL-with- verification paradigm provides the training methodology.

Introduction to Lean 4

If mathematics is the language of certainty, then Lean 4 is its compiler. In this section we give a self-contained, tutorial-style introduction to Lean 4, the interactive theorem prover that has become the de facto standard platform for AI-assisted formal mathematics. We assume no prior experience with dependent type theory; every concept is built from the ground up with worked examples.

Propositions as Types, Proofs as Programs

The philosophical foundation of Lean is the Curry–Howard correspondence: every mathematical proposition is a type, and every proof of that proposition is a term (program) inhabiting that type.

Let us see this in action with the simplest possible theorem:

theorem two_plus_two : 2 + 2 = 4 := by
  rfl

theorem self_implication (P : Prop) : P -> P := by
  intro h    -- assume P holds; call the proof h
  exact h    -- provide h as the proof of the goal P

The Type Hierarchy

Lean organises types into a hierarchy of universes:

Natural Numbers and Induction

The natural numbers are defined as an inductive type:

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

Every natural number is either zero or the successor of another natural number. This gives us the recursor (induction principle) for free.

theorem Nat.rec_on {P : Nat -> Prop}
  (n : Nat) (h0 : P 0) (hs : forall  k, P k -> P (k + 1)) : P n

theorem add_comm (n m : Nat) : n + m = m + n := by
  induction n with
  | zero => simp
  | succ k ih =>
    simp [Nat.succ_add, Nat.add_succ]
    exact ih

theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction c with
  | zero => simp
  | succ k ih =>
    simp [Nat.add_succ]
    exact ih

Logic in Lean

Lean defines logical connectives as inductive types:

-- Conjunction (And)
structure And (P Q : Prop) where
  left  : P
  right : Q

-- Disjunction (Or)
inductive Or (P Q : Prop) where
  | inl (h : P) : Or P Q
  | inr (h : Q) : Or P Q

-- Negation
def Not (P : Prop) : Prop := P -> False

-- Existential
inductive Exists {A : Type} (P : A -> Prop) where
  | intro (w : A) (h : P w) : Exists P

theorem and_comm (P Q : Prop) : P / Q -> Q / P := by
  intro <hp, hq>    -- destructure the And pair
  exact <hq, hp>    -- construct the swapped pair

theorem or_comm (P Q : Prop) : P \/ Q -> Q \/ P := by
  intro h
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

theorem modus_tollens (P Q : Prop) :
    (P -> Q) -> Not Q -> Not P := by
  intro hpq hnq hp
  exact hnq (hpq hp)

theorem exists_even : exists  n : Nat, n 
  use 42
  rfl

The Tactic Language

Tactics are commands that transform proof goals. Each tactic takes the current goal and produces zero or more subgoals. A proof is complete when no goals remain.

We now survey the most important tactics with examples.

intro.

Introduces a hypothesis or universally quantified variable.

-- Goal: forall  n : Nat, n = n
-- After 'intro n': Goal becomes n = n with n : Nat in context

exact.

Provides the exact proof term for the current goal.

-- Goal: P    Context: h : P
-- 'exact h' closes the goal

apply.

Applies a function or lemma to the goal, generating subgoals for its arguments.

-- Goal: Q    Context: h : P -> Q
-- 'apply h' changes goal to P

rw (rewrite).

Rewrites the goal using an equality.

-- Goal: a + 0 = a
-- 'rw [Nat.add_zero]' rewrites to a = a, then rfl closes it

simp.

The simplifier: applies a collection of rewrite rules repeatedly until no more apply. Lean ships with hundreds of @[simp] lemmas.

-- simp can solve: 0 + n = n, n * 1 = n, True / P <-> P, etc.
example (n : Nat) : 0 + n = n := by simp

ring.

Proves equalities in commutative (semi)rings by normalisation.

example (a b : Int) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

omega.

Decides linear arithmetic over natural numbers and integers.

example (n m : Nat) (h : n < m) : n + 1 <= m := by omega

cases.

Performs case analysis on an inductive type.

theorem zero_or_succ (n : Nat) : n = 0 \/ exists  m, n = m + 1 := by
  cases n with
  | zero => left; rfl
  | succ m => right; exact <m, rfl>

induction.

Performs structural induction on an inductive type.

constructor.

Applies the constructor of an inductive type to split a goal.

-- Goal: P / Q
-- 'constructor' splits into two goals: P and Q

have.

Introduces an intermediate result (a local lemma).

-- 'have h : P := proof_of_P' adds h : P to the context

calc.

Writes a calculation-style proof as a chain of equalities or inequalities.

example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  calc a = b := h1
    _ = c := h2

Dependent Types

The real power of Lean comes from dependent types: types that depend on values.

inductive Vec (A : Type) : Nat -> Type where
  | nil  : Vec A 0
  | cons : A -> Vec A n -> Vec A (n + 1)

def Vec.head : Vec A (n + 1) -> A
  | .cons a _ => a

Structures and Typeclasses

Lean organises mathematical abstractions using typeclasses, a mechanism borrowed from Haskell but extended with dependent types.

class Group (G : Type) extends Mul G, One G, Inv G where
  mul_assoc : forall  a b c : G, a * b * c = a * (b * c)
  one_mul   : forall  a : G, 1 * a = a
  inv_mul   : forall  a : G, a^(-1) * a = 1

-- This theorem works for ANY group, not just a specific one
theorem mul_right_cancel [Group G] (a b c : G)
    (h : a * c = b * c) : a = b := by
  have : a * c * c^(-1) = b * c * c^(-1) := by rw [h]
  simp [mul_assoc, mul_inv_cancel] at this
  exact this

The Three Axioms

Lean 4's kernel is constructive, but Lean adds three axioms to support classical mathematics:

1. Propositional extensionality: if $P\leftrightarrow Q$ then $P=Q$.

   axiom propext : (P <-> Q) -> P = Q
       

2. Quotient types: given an equivalence relation on a type, form the type of equivalence classes.

3. Choice: for any non-empty type, there exists a choice function.

   axiom Classical.choice : Nonempty A -> A
       

What Cannot Be Formalised?

A natural question arises: can everything be formalised in Lean?

Exercises

Lean 4 by Example

We now work through extended examples that demonstrate how real mathematics is formalised in Lean 4. Each example builds on the foundations from Introduction to Lean 4, gradually introducing Mathlib and more advanced techniques.

Elementary Number Theory

-- Prove that 3 divides 12
example : 3 | 12 := <4, rfl>

-- Transitivity of divisibility
theorem dvd_trans (a b c : Nat)
    (h1 : a | b) (h2 : b | c) : a | c := by
  obtain <k, hk> := h1
  obtain <m, hm> := h2
  exact <k * m, by rw [hm, hk]; ring>

import Mathlib.Data.Nat.GCD.Basic

-- Bezout: there exist integers a, b such that
-- a * m + b * n = gcd m n
#check Nat.gcd_eq_gcd_ab  -- the Bezout lemma in Mathlib

import Mathlib.Data.Nat.Prime.Basic

-- Euclid's theorem: for every n, there exists a prime > n
theorem exists_infinite_primes (n : Nat) :
    exists  p, n < p / Nat.Prime p := by
  -- Consider n! + 1
  let N := Nat.factorial n + 1
  -- N >= 2, so it has a prime factor
  have hN : 2 <= N := by omega
  obtain <p, hp_prime, hp_dvd> := Nat.exists_prime_and_dvd
    (by omega : N != 1)
  use p
  constructor
  * -- Show p > n
    by_contra h
    push_neg at h
    -- p <= n, so p divides n!
    have : p | Nat.factorial n :=
      hp_prime.dvd_factorial.mpr h
    -- p divides N and n!, so p divides N - n! = 1
    have : p | 1 := by
      have := Nat.dvd_sub' hp_dvd this
      simp at this; exact this
    -- But p >= 2, contradiction
    exact Nat.Prime.one_lt hp_prime |>.not_le
      (Nat.le_of_dvd one_pos this)
  * exact hp_prime

Real Analysis

Lean's Mathlib library formalises real analysis using filters, an elegant abstraction that unifies limits of sequences, functions, and topological convergence.

-- Filter.Tendsto f atTop (nhds L)
-- means: f(n) -> L as n -> infinity

import Mathlib.Analysis.SpecificLimits.Basic

example : Filter.Tendsto (fun n : Nat => (1 : Real) / n)
    Filter.atTop (nhds 0) := by
  exact tendsto_const_div_atTop_nhds_0_nat 1

-- If a_n <= b_n <= c_n and a_n -> L and c_n -> L, then b_n -> L
theorem squeeze_theorem
    {a b c : Nat -> Real} {L : Real}
    (hab : forall  n, a n <= b n)
    (hbc : forall  n, b n <= c n)
    (ha : Filter.Tendsto a Filter.atTop (nhds L))
    (hc : Filter.Tendsto c Filter.atTop (nhds L)) :
    Filter.Tendsto b Filter.atTop (nhds L) := by
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le ha hc
  * exact eventually_of_forall hab
  * exact eventually_of_forall hbc

Linear Algebra

import Mathlib.LinearAlgebra.Basic

-- R-module structure provides:
-- * Addition: v + w
-- * Scalar multiplication: r * v
-- * Module axioms (distributivity, associativity, etc.)

-- Example: R^n as a module
example : Module Real (Fin 3 -> Real) := inferInstance

-- A linear map preserves addition and scalar multiplication
-- LinearMap R M N is the type of R-linear maps from M to N

-- The kernel of a linear map
#check LinearMap.ker  -- Submodule R M

-- The rank-nullity theorem
#check LinearMap.finrank_range_add_finrank_ker
-- : finrank (range f) + finrank (ker f) = finrank M

Group Theory

import Mathlib.GroupTheory.Lagrange

-- Lagrange's theorem: |H| divides |G|
#check Subgroup.card_subgroup_dvd_card
-- : card H | card G

-- A consequence: the order of an element divides |G|
#check orderOf_dvd_card

Working with Mathlib

Searching for lemmas.

Lean 4 provides several tactics for discovering relevant lemmas:

-- exact? : searches for a single lemma that closes the goal
-- apply? : searches for a lemma whose conclusion matches the goal
-- simp?  : runs simp and reports which lemmas were used
-- rw?    : searches for a rewrite rule

example (n : Nat) (h : n > 0) : n != 0 := by
  exact?  -- suggests: exact Nat.pos_iff_ne_zero.mp h

Common Pitfalls and Debugging

Universe errors.

Lean's universe polymorphism can produce confusing errors:

-- ERROR: universe level mismatch
-- This often occurs when mixing Prop and Type
-- Fix: use 'universe u' declarations or explicit annotations

Typeclass inference failures.

When Lean cannot find an instance:

-- ERROR: failed to synthesize instance
--   CommRing (Matrix (Fin 2) (Fin 2) Nat)
-- Fix: ensure the right imports and instance declarations

Definitional vs. propositional equality.

-- 2 + 2 = 4 is DEFINITIONAL (rfl works)
-- n + 0 = n is PROPOSITIONAL (requires induction proof)
-- This distinction trips up beginners and AI models alike

A Complete Worked Example: The Irrationality of $\sqrt{2}$

We conclude with a complete, annotated proof of a classical result.

import Mathlib.Data.Rat.Sqrt
import Mathlib.Data.Int.Parity

theorem sqrt_two_irrational : Irrational (Real.sqrt 2) := by
  rw [irrational_sqrt_two]
  -- Mathlib already has this! But let us sketch the structure:
  -- 1. Assume sqrt 2 = p / q, coprime
  -- 2. Then 2 * q^2 = p^2
  -- 3. p^2 even => p even => p = 2k
  -- 4. 2 * q^2 = 4 * k^2 => q^2 = 2 * k^2
  -- 5. q^2 even => q even
  -- 6. Contradiction with coprimality

The Compilation Pipeline and Performance

Lean 4 is unique among theorem provers in being a compiled language.

Further Exercises

Lean 4 Advanced Topics and Practical Formalization

The preceding sections introduced Lean 4 as a language and sketched its role in the AI-for-mathematics pipeline. We now dive substantially deeper. Our goals in this section are threefold: (1) to explain the dependent type theory that makes Lean 4 expressive enough to state any theorem in mathematics; (2) to survey the tactic language that makes proving those theorems feasible; and (3) to walk through two extended worked examples that show what real formalization looks like in practice.

Readers who have never touched a proof assistant may find the first subsection challenging. We encourage persistence: the payoff is a precise understanding of what it means for a computer to verify a mathematical argument, and that understanding is essential for appreciating the generative models discussed in the remainder of this chapter.

Dependent Types in Depth

In a simply-typed language such as Haskell or OCaml, the type of a function can depend on other types (polymorphism), but it cannot depend on values. Dependent type theory removes this restriction: types may mention ordinary terms. The canonical first example is a vector of known length.

inductive Vec (alpha : Type) : Nat -> Type where
  | nil  : Vec alpha 0
  | cons : alpha -> Vec alpha n -> Vec alpha (n + 1)

Why does this matter for formalization? Because mathematical objects often carry constraints that are part of their identity. A matrix in ${\mathrm{ℝ}}^{m\times n}$ has $m$ rows and $n$ columns; a permutation on $\{1,\dots ,n\}$ has exactly $n!$ elements; a probability distribution over a finite set sums to one. Dependent types let us encode these constraints directly in the type, so that ill-formed objects are not merely flagged at runtime but are literally impossible to construct.

def Matrix (m n : Type) (alpha : Type) := m -> n -> alpha

def Matrix.mul [Fintype n] [Mul alpha] [AddCommMonoid alpha]
    (A : Matrix m n alpha) (B : Matrix n p alpha) : Matrix m p alpha :=
  fun i k => sum j, A i j * B j k

More generally, a dependent function type (also called a Pi-type) has the form $$\mathrm{\Pi }(x:A),B(x),$$ where $B$ is a family of types indexed by elements of $A$. In Lean 4 syntax this is written (x : A) \(\) B x. When $B$ does not actually depend on $x$, the Pi-type reduces to the ordinary function type $A\to B$. At the other extreme, when $A$ is Prop and $B$ maps each proposition to its proof type, the Pi-type encodes universal quantification: “for all $x:A$, $B(x)$ holds” is precisely $\mathrm{\Pi }(x:A),B(x)$.

The dual notion is the Sigma-type $\mathrm{\Sigma }(x:A),B(x)$, which packages a value $x:A$ together with a witness of type $B(x)$. This encodes existential quantification: “there exists $x:A$ such that $B(x)$ holds” becomes $\mathrm{\Sigma }(x:A),B(x)$.

Inductive Types and Pattern Matching

Lean 4 follows the tradition of Martin-Löf type theory in building complex data types from inductive definitions. An inductive type is specified by listing its constructors, each of which may take arguments, including recursive references to the type being defined. The canonical example is the natural numbers.

inductive Nat where
  | zero : Nat
  | succ : Nat -> Nat

This says: a natural number is either zero or the successor of another natural number. From this single definition, Lean derives an induction principle, a recursion principle, and decidable equality. Pattern matching on the constructors gives us structural recursion:

def add : Nat -> Nat -> Nat
  | m, .zero   => m
  | m, .succ n => .succ (add m n)

The termination checker verifies that the recursive call add m n decreases on the second argument, ensuring that the function is total.

Lists, binary trees, and abstract syntax trees all follow the same pattern:

inductive List (alpha : Type) where
  | nil  : List alpha
  | cons : alpha -> List alpha -> List alpha

inductive BinTree (alpha : Type) where
  | leaf : BinTree alpha
  | branch : BinTree alpha -> alpha -> BinTree alpha -> BinTree alpha

For formalization, the most important inductive types are the propositions. In Lean 4, the logical connectives are themselves inductively defined:

-- Conjunction (already in core)
structure And (a b : Prop) : Prop where
  intro ::
  left  : a
  right : b

-- Disjunction (already in core)
inductive Or (a b : Prop) : Prop where
  | inl : a -> Or a b
  | inr : b -> Or a b

A proof of $A\wedge B$ is a pair of proofs (one for $A$, one for $B$); a proof of $A\vee B$ is either a proof of $A$ or a proof of $B$, tagged to say which case holds. This is the Curry–Howard correspondence made concrete: logical connectives are type constructors, and proofs are data.

Tactics in Depth

A tactic in Lean 4 is a metaprogram that transforms the current proof state (a list of goals, each consisting of a local context and a target type) into a new proof state with fewer or simpler goals. When no goals remain, the proof is complete. Lean 4 ships with a rich library of built-in tactics, and Mathlib adds many more. We survey the most important ones.

The simp Tactic and the Simp Lemmas Database

The simp tactic is the workhorse of Lean 4 formalization. It applies a configurable set of rewrite rules (called simp lemmas) to simplify the goal. A simp lemma is any lemma tagged with the @[simp] attribute; Mathlib contains thousands of such lemmas.

@[simp] theorem Nat.add_zero (n : Nat) : n + 0 = n := ...
@[simp] theorem List.length_nil : [].length = 0 := ...
@[simp] theorem Bool.not_not (b : Bool) : !!b = b := ...

When invoked, simp repeatedly applies matching simp lemmas until no further simplification is possible. It can also unfold definitions, apply congruence rules, and use hypotheses from the local context:

example (n : Nat) : n + 0 + 0 = n := by simp
example (xs : List alpha) : (xs ++ []).length = xs.length := by simp
example (h : a = b) : a + c = b + c := by simp [h]

The variant simp only [lemma1, lemma2] restricts simplification to an explicit list of lemmas, which is useful when the full simp set produces undesirable results or when performance matters.

The omega Tactic

The omega tactic decides the theory of linear arithmetic over the integers and natural numbers. It can prove any goal that is a Boolean combination of linear inequalities and equalities:

example (n m : Nat) (h : n < m) : n + 1 <= m := by omega
example (a b : Int) (h1 : a <= b) (h2 : b <= a) : a = b := by omega
example (x : Nat) : x / 2 + x / 2 + x 

Under the hood, omega implements the Omega test of Pugh [76], which decides Presburger arithmetic by quantifier elimination. The implementation in Lean 4 is a verified decision procedure: the tactic produces a proof term that the kernel can check, so the correctness of omega does not enlarge the trusted computing base.

The ring Tactic

The ring tactic proves equalities in commutative (semi)rings by normalizing both sides to a canonical form (a sum of monomials sorted lexicographically) and checking syntactic equality:

example (a b : Int) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring
example (x y z : Rat) : x*(y+z) - x*y - x*z = 0 := by ring
example (n : Nat) : n*(n+1)/2 + (n+1) = (n+1)*(n+2)/2 := by ring

The ring tactic works for any type that is an instance of the CommRing (or CommSemiring) type class. This includes integers, rationals, reals, complex numbers, and polynomials.

The norm_num Tactic

The norm_num tactic evaluates numerical expressions and proves numerical facts:

example : (7 : Nat) * 13 = 91 := by norm_num
example : (2 : Real)^10 = 1024 := by norm_num
example : Nat.Prime 104729 := by norm_num
example : Not  Nat.Prime 91 := by norm_num

Beyond simple arithmetic, norm_num supports an extensible plugin system: Mathlib registers plugins for primality testing, divisibility checks, modular arithmetic, and more. Each plugin produces a verified proof certificate, so the kernel trusts only its own type-checking, not the plugin's computation.

The polyrith Tactic

The polyrith tactic proves polynomial arithmetic goals by calling an external oracle (typically a Gröbner basis computation via SageMath or a similar system) to find a certificate, then verifying the certificate within Lean:

example (a b c : Rat) (h1 : a + b + c = 0) (h2 : a*b + b*c + a*c = -1) :
    a^2 + b^2 + c^2 = 2 := by polyrith

This is a powerful example of the oracle pattern: the hard computational work (finding the certificate) is done by an untrusted external tool, while the easy verification work (checking the certificate) is done by the trusted kernel. The correctness of the overall proof depends only on the kernel, not on SageMath.

The aesop Tactic

The aesop tactic (Automated Extensible Search for Obvious Proofs) performs a best-first tree search over a configurable set of rules. It can apply lemmas, introduction rules, elimination rules, simp lemmas, and custom user-defined rules. It is particularly effective for closing goals that require a combination of case splitting, simplification, and hypothesis application:

example (h : a in s union t) (hs : s subset u) (ht : t subset u) : a in u := by aesop

Mathlib tags many lemmas with @[aesop safe], @[aesop unsafe 50%], etc., to guide aesop's search. The percentages indicate the tactic's confidence that a rule will be useful, influencing the search priority.

example (x : alpha) (s t u : Set alpha) (h : x in s inter (t union u)) :
    x in (s inter t) union (s inter u) := by aesop

The decide Tactic

The decide tactic works on propositions $P$ for which Lean can find an instance of Decidable P. It evaluates the decision procedure and, if the result is true, extracts a proof:

example : 2 + 3 = 5 := by decide
example : Not  (3 | 7) := by decide
example : Finset.card {1, 2, 3, 4, 5} = 5 := by decide

The decide tactic is conceptually simple but can be slow for large computations because it runs the decision procedure inside the kernel. For numerical facts, norm_num is almost always faster because it produces compact proof certificates rather than evaluating step by step.

Writing Custom Tactics

Because Lean 4 is a general-purpose programming language, its tactic framework is not a separate language bolted on top: it is ordinary Lean code that manipulates proof states. A tactic is a function of type TacticM Unit, where TacticM is a monad that provides access to the current goal, the local context, and the ability to create new metavariables.

The simplest custom tactic is one that wraps existing tactics with additional logic:

/-- A tactic that tries `simp`, then `omega`, then `ring`. -/
syntax "auto_close" : tactic
macro_rules
  | `(tactic| auto_close) =>
    `(tactic| first | simp | omega | ring)

More sophisticated tactics can inspect the goal, pattern-match on its structure, and decide which strategy to use:

elab "smart_arith" : tactic => do
  let goal <- Lean.Elab.Tactic.getMainTarget
  if goal.isAppOf ``Eq then
    -- Try ring for equalities
    Lean.Elab.Tactic.evalTactic (<- `(tactic| ring))
  else
    -- Try omega for inequalities
    Lean.Elab.Tactic.evalTactic (<- `(tactic| omega))

This ability to program new tactics is what makes Lean 4 uniquely suited to AI-driven formalization: a generative model can output not only proofs but also custom tactics that encode proof strategies [9].

Metaprogramming in Lean 4

Lean 4's metaprogramming framework operates at three levels, each offering increasing power and complexity.

Syntax extensions and notations.

Lean 4 allows users to define new syntax using the syntax, notation, and macro commands. For example, Mathlib defines the notation ${\sum }_{i\in s}f(i)$ as:

notation "sum" i " in " s ", " f => Finset.sum s (fun i => f)

Macros.

A macro is a syntax transformation that runs before elaboration. Macros can pattern-match on syntax objects and produce new syntax:

macro "square" x:term : term => `($x * $x)

#eval square 7  -- outputs 49

Elaboration-time metaprogramming.

For full control, users can write elaborators: Lean functions that run during type-checking and can inspect the environment, create metavariables, unify types, and build terms. This is the mechanism used to implement tactics, derive handlers, and the entirety of the tactic mode.

The elaboration pipeline proceeds in stages:

1. Parsing: source text is converted to a concrete syntax tree (CST).

2. Macro expansion: macros are expanded until no more macros apply.

3. Elaboration: the CST is converted to a fully-typed core expression, with metavariables for missing information.

4. Type inference and unification: metavariables are solved by unification constraints.

5. Kernel type-checking: the final expression is checked by the trusted kernel.

Worked Example: Formalizing the Bolzano–Weierstrass Theorem

We now present a detailed worked example that illustrates the full workflow of formalizing a nontrivial result in real analysis. We chose the Bolzano–Weierstrass theorem because it is well-known, conceptually rich, and exercises several features of Lean 4 and Mathlib simultaneously.

The Informal Statement and Proof

Setting Up the Lean Formalization

The first task is to identify the relevant Mathlib concepts. In Mathlib, a sequence of reals is simply a function $a:\mathbb{N}\to ℝ$. Boundedness is expressed via the predicate Bornology.IsBounded or equivalently by asserting that the range of $a$ lies in some interval. A subsequence is encoded using a strictly increasing function $\phi :\mathbb{N}\to \mathbb{N}$, and the subsequence itself is $a\circ \phi$. Convergence is expressed via the filter Filter.Tendsto.

import Mathlib.Topology.Sequences
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Topology.Order.Basic

open Filter Topology

The Formal Statement

The Bolzano–Weierstrass theorem already exists in Mathlib as IsCompact.tendsto_subseq, which states that a sequence in a compact set has a convergent subsequence. For pedagogical purposes, we specialize this to the real numbers:

theorem bolzano_weierstrass
    (a : Nat -> Real)
    (hbdd : exists  M : Real, forall  n, |a n| <= M) :
    exists  (phi : Nat -> Nat), StrictMono phi /
      exists  (l : Real), Tendsto (a  o  phi) atTop (nhds l) := by
  sorry -- to be filled in

Let us unpack the statement. The hypothesis hbdd says that there exists a bound $M$ such that $|a_n|\le M$ for all $n$. The conclusion asserts the existence of a strictly increasing function $\phi$ (the subsequence indices) and a limit $\ell$ such that $a\circ \phi$ converges to $\ell$ in the neighborhood filter $𝒩(\ell )$.

Walking Through the Proof

The proof strategy in Lean mirrors the informal proof but uses the more general Mathlib machinery of compact sets:

theorem bolzano_weierstrass
    (a : Nat -> Real)
    (hbdd : exists  M : Real, forall  n, |a n| <= M) :
    exists  (phi : Nat -> Nat), StrictMono phi /
      exists  (l : Real), Tendsto (a  o  phi) atTop (nhds l) := by
  -- Step 1: Extract the bound M
  obtain <M, hM> := hbdd
  -- Step 2: The range of a lies in the closed ball [-M, M]
  have hrange : forall  n, a n in Set.Icc (-M) M := by
    intro n
    constructor
    * linarith [abs_le.mp (hM n)]
    * linarith [abs_le.mp (hM n)]
  -- Step 3: The closed interval [-M, M] is compact
  have hcpt : IsCompact (Set.Icc (-M) M) :=
    isCompact_Icc
  -- Step 4: Apply the sequential compactness theorem
  obtain <l, hlmem, phi, hphimono, hphitend> :=
    hcpt.tendsto_subseq hrange
  -- Step 5: Package the result
  exact <phi, hphimono, l, hphitend>

Let us examine each step:

• Step 1 (obtain): Destructs the existential hypothesis to get a concrete $M$ and a proof hM that $|a_n|\le M$ for all $n$.

• Step 2 (have): Shows that each $a_n$ lies in $[-M,M]$. The key Mathlib lemma abs_le converts $|x|\le M$ into $-M\le x\wedge x\le M$. The linarith tactic handles the linear arithmetic.

• Step 3 (have): Appeals to the Mathlib lemma isCompact_Icc, which states that closed bounded intervals in $\mathrm{ℝ}$ are compact. This is where the Heine–Borel theorem is hiding.

• Step 4 (obtain): This is the core step. The lemma IsCompact.tendsto_subseq states that if $K$ is compact and $a_n\in K$ for all $n$, then there exist $\ell \in K$, a strictly increasing $\phi$, and a proof that $a\circ \phi \to \ell$.

• Step 5 (exact): Repackages the extracted data into the form required by the goal.

Worked Example: Formalizing Lagrange's Theorem

Our second worked example comes from algebra. Lagrange's theorem is one of the first nontrivial results in group theory.

Informal Proof Sketch

The key idea is to partition $G$ into left cosets of $H$: the sets $gH=\{gh:h\in H\}$ for each $g\in G$. The cosets are pairwise disjoint and each has exactly $|H|$ elements (because the map $h\mapsto gh$ is a bijection $H\to gH$). Since $G$ is the disjoint union of its cosets, $$|G|=[\text{number of cosets}]\times |H|,$$ so $|H|$ divides $|G|$.

The Lean Formalization

In Mathlib, finite groups are modeled using the Fintype type class, and subgroups are terms of type Subgroup G. The cardinality of a finite type is Fintype.card. Lagrange's theorem is already proved in Mathlib:

import Mathlib.GroupTheory.Coset
import Mathlib.GroupTheory.Index

variable {G : Type*} [Group G] [Fintype G]
  (H : Subgroup G) [Fintype H]

-- The Mathlib statement:
-- Subgroup.card_subgroup_dvd_card : Fintype.card H | Fintype.card G

-- We can also state it ourselves and prove it from Mathlib:
theorem lagrange :
    Fintype.card H | Fintype.card G := by
  exact Subgroup.card_subgroup_dvd_card H

While the one-line proof is anticlimactic, the point is that Mathlib has already done the heavy lifting. Let us examine what lies beneath card_subgroup_dvd_card. The proof chain involves:

1. The quotient $G/H$ (the set of left cosets) is a Fintype.

2. There is a bijection between $G$ and $G/H\times H$ (the coset partition).

3. The cardinality of a product type is the product of the cardinalities.

4. Therefore $|G|=|G/H|\times |H|$, and $|H|||G|$.

If we want to see more of the proof structure, we can unfold one layer:

theorem lagrange_detailed :
    Fintype.card H | Fintype.card G := by
  rw [Subgroup.card_eq_card_quotient_mul_card_subgroup]
  exact dvd_mul_left (Fintype.card H) (Fintype.card (G / H))

Here, card_eq_card_quotient_mul_card_subgroup is the key identity $|G|=|G/H|\times |H|$, and dvd_mul_left witnesses that $|H|$ divides $|G/H|\times |H|$.

Lessons from the Two Examples

Both worked examples illustrate a common pattern in modern formalization. The informal mathematical argument is restructured to match the abstractions available in the library. In the Bolzano–Weierstrass example, we did not implement the nested-intervals construction; instead, we recognized that the key abstraction is compactness and appealed to a general theorem about compact sets. In the Lagrange example, we did not construct the coset partition; instead, we appealed to a theorem about the cardinality of quotient types.

This pattern has a direct implication for AI: a generative model that can map informal proof strategies to the right library abstractions will produce short, elegant formalizations. A model that tries to translate informal proofs literally will produce verbose, brittle code that duplicates existing library content. The ability to search the library effectively is therefore at least as important as the ability to generate tactic sequences [9].

Performance and Compilation

Lean 4 compiles to native code via C, and its compiler is designed to handle large libraries efficiently. Several design choices contribute to performance:

Incremental compilation.

Lean 4 uses a file-level incremental compilation model: each .lean file is compiled independently, and only files whose dependencies have changed are recompiled. This is crucial for Mathlib, which consists of over 4,000 files totaling more than one million lines of code.

Reference counting.

Instead of garbage collection, Lean 4 uses reference counting with a “reset–reuse” optimization: when the last reference to an object is consumed, the memory is reused in place rather than freed and reallocated. This makes functional programming competitive with imperative code for many workloads.

Lazy evaluation of proofs.

Lean 4 does not evaluate proof terms during compilation (proofs are erased from the compiled output). This means that a file can import thousands of theorems without paying any runtime cost for the proofs; only the types (statements) are retained.

Parallel checking.

The Lean 4 server supports parallel elaboration: different declarations within a file can be type-checked concurrently. On modern hardware with many cores, this significantly reduces the wall-clock time for checking large files.

Exercises for Section 6

Other Theorem Provers – A Comparative Survey

Lean 4 is the newest entrant in a field with a history stretching back to the 1960s. Understanding the broader landscape of theorem provers is important for three reasons. First, many of the ideas now appearing in Lean (dependent types, tactic languages, large formal libraries) were pioneered in older systems. Second, significant bodies of formalized mathematics exist in systems other than Lean, and AI systems that can work with multiple provers have access to a much larger training corpus. Third, the design choices made by different provers illuminate genuine trade-offs in foundations, automation, and usability.

This section surveys seven major theorem provers, then presents a systematic comparison. We close with a discussion of whether the field is converging on a single system or whether diversity will persist.

Coq (Rocq)

Coq (recently rebranded as Rocq for trademark reasons) is the oldest actively developed proof assistant based on dependent type theory [77]. Development began at INRIA in 1984 under Thierry Coquand and Gérard Huet, with the first public release in 1989. Coq is based on the Calculus of Inductive Constructions (CIC), the same foundation as Lean 4, and for decades it was the de facto standard for constructive formalization.

Key features.

• Gallina and Ltac. Coq's specification language is Gallina (a functional language similar to OCaml), and its tactic language is Ltac (or the newer Ltac2). Unlike Lean 4, where tactics and terms live in the same language, Coq maintains a sharper separation between the specification language and the tactic language.

• Extraction. Coq can extract verified programs to OCaml, Haskell, or Scheme. This feature has been used to produce verified compilers and verified cryptographic implementations.

• Universes. Coq supports a cumulative universe hierarchy with universe polymorphism, similar to Lean 4.

SSReflect.

SSReflect (“Small Scale Reflection”) is a proof methodology and Coq library developed by Georges Gonthier for the formalization of the Four Color Theorem [15]. The key idea is to represent propositions as Boolean computations whenever possible, so that many proof obligations reduce to computation (“reflection”) rather than deduction. SSReflect introduces a distinctive proof style with small, composable tactics and extensive use of Boolean reflection. The Mathematical Components library (MathComp) is the modern incarnation of this approach.

Major achievements.

• Four Color Theorem (Gonthier, 2005) [15]: the first formalization of a famous theorem whose original proof relied on computer case analysis.

• Odd Order Theorem (Gonthier et al., 2013) [16]: a 150-page proof in algebra, requiring approximately 170,000 lines of Coq code and six years of work.

• CompCert (Leroy, 2006) [17]: a verified optimizing C compiler. CompCert's significance extends beyond mathematics: it demonstrated that formal verification could produce software competitive with industrial compilers.

• Feit–Thompson Theorem: identical to the Odd Order Theorem, formalized as part of the MathComp project.

Isabelle/HOL

Isabelle is a generic proof assistant framework developed by Lawrence Paulson at Cambridge and Tobias Nipkow at Munich [64]. The most widely used instantiation is Isabelle/HOL, which implements classical higher-order logic (HOL). Unlike Lean and Coq, which are based on dependent type theory, Isabelle/HOL uses a simpler type system (simple type theory with type classes and limited polymorphism) that trades some expressiveness for stronger automation.

Key features.

• Sledgehammer. Sledgehammer is Isabelle's flagship automation tool. Given a proof goal, Sledgehammer sends it to one or more external automated theorem provers (E, Vampire, Z3, SPASS) and, if any of them finds a proof, reconstructs the proof within Isabelle using trusted internal methods [18]. Sledgehammer dramatically reduces the manual effort of formalization and is one of the main reasons Isabelle/HOL remains competitive despite its simpler type system.

• Isar proof language. Isabelle's structured proof language, Isar (“Intelligible Semi-Automated Reasoning”), produces proofs that read almost like informal mathematics. An Isar proof states intermediate claims with have and show, provides justifications with by, and structures case analysis with consider and obtain.

• Archive of Formal Proofs (AFP). The AFP is a curated, peer-reviewed collection of Isabelle formalizations, containing over 800 entries and millions of lines of code. It functions as a journal of formalized mathematics and computer science.

Major achievements.

• Kepler Conjecture (Hales et al., 2017) [19]: the proof that the face-centered cubic packing is the densest sphere packing in three dimensions. The original computer-assisted proof by Hales (1998) was controversial; the Isabelle/HOL formalization (the Flyspeck project) settled the matter definitively.

• seL4 (Klein et al., 2009) [20]: a verified microkernel operating system. The proof establishes that the C code of seL4 correctly implements its abstract specification, ruling out entire classes of bugs (buffer overflows, null pointer dereferences, etc.).

• Prime Number Theorem (Avigad et al., 2007; Eberl, 2018): formalized within the AFP with full analytic number theory proofs.

Proof style.

An Isabelle/HOL proof in Isar style reads remarkably like informal mathematics. Consider the following proof that the square root of 2 is irrational (sketch):

theorem sqrt2_irrational: "sqrt 2 notin Rat"
proof (rule ccontr)
  assume "Not  sqrt 2 notin Rat"
  then obtain p q :: nat where
    "q != 0" and "sqrt 2 = p / q" and "coprime p q"
    by (auto simp: Rats_def)
  then have "2 * q^2 = p^2"
    by (auto simp: power2_eq_square field_simps)
  then have "even p" by arith
  ...
qed

Agda

Agda is a dependently typed programming language and proof assistant developed primarily by Ulf Norell at Chalmers University [78]. Like Lean 4, Agda is based on Martin-Löf type theory (MLTT), but it makes different design choices that give it a distinctive character.

Key features.

• No tactics. Agda traditionally does not have a tactic mode. Proofs are written as ordinary programs using pattern matching and recursion. The Agda.Auto module provides some automation, and recent versions support “auto” and “refine” commands, but the culture remains term-oriented rather than tactic-oriented.

• Unicode-heavy syntax. Agda embraces Unicode: operators like $\forall$, $\lambda$, $\to$, $\times$, and $\equiv$ are used directly in source code. Combined with mixfix operators, this makes Agda code visually close to mathematical notation.

• Cubical Agda. Cubical Agda extends the language with primitives from cubical type theory, providing a computational interpretation of the univalence axiom from homotopy type theory (HoTT). In cubical Agda, the statement “isomorphic types are equal” is not merely an axiom but a theorem with computational content: transporting a proof along an isomorphism actually computes. This is a feature that no other major proof assistant offers.

Limitations.

Agda's standard library is much smaller than Mathlib, MathComp, or the AFP, which limits its use for large-scale formalization projects. Automation is weaker than in Lean or Isabelle, making proofs more verbose. The community, while passionate, is significantly smaller than Lean's or Coq's.

Contributions.

Agda has been influential in the development of HoTT and as a testbed for advanced type-theoretic features. The HoTT library in Agda contains formalizations of fundamental results in synthetic homotopy theory.

Mizar

Mizar is a proof assistant and a formal language developed by Andrzej Trybulec at the University of Bialystok, with roots going back to 1973 [60]. Mizar takes a fundamentally different approach from the type-theoretic systems: it is based on first-order logic with Tarski–Grothendieck set theory.

Key features.

• Natural language style. Mizar proofs are written in a stylized but readable English-like syntax. A typical Mizar proof reads: “Let $x$ be a real number. Assume $x>0$. Then $x^2>0$ by SQUARE_1:72.” The references (like SQUARE_1:72) point to specific theorems in the Mizar Mathematical Library (MML).

• Large formal library. The MML contains over 60,000 theorems and has been under continuous development since the 1980s. It covers a broad range of mathematics, from basic set theory to functional analysis and topology.

• Set-theoretic foundation. Unlike type-theoretic systems, Mizar works directly with sets, functions, and first-order logic. This can be more natural for mathematicians trained in the ZFC tradition.

Limitations.

Mizar's tooling is dated compared to Lean, Coq, or Isabelle. It lacks a modern IDE, has limited metaprogramming capabilities, and its community has contracted in recent years. The MML is not easily interoperable with other systems.

Relevance to AI.

Despite its age, Mizar has contributed to AI research through the Mizar Problems for Theorem Proving (MPTP) project, which extracted thousands of proof obligations from the MML and encoded them in first-order TPTP format. These problems have served as benchmarks for automated theorem provers and, more recently, for neural theorem proving systems. The natural-language-like proof format of Mizar has also inspired work on autoformalization: translating informal mathematical text into formal Mizar proofs [79].

HOL Light and HOL4

The HOL family of theorem provers (“Higher Order Logic”) descends from Mike Gordon's original HOL system at Cambridge [80]. The two most active descendants are HOL Light (maintained by John Harrison) and HOL4 (maintained by a community effort).

HOL Light.

HOL Light is notable for its tiny trusted kernel: approximately 400 lines of OCaml code implement the entire inference engine. This minimalism makes it exceptionally trustworthy. HOL Light was the system used for the Flyspeck project's core formalization (alongside Isabelle), and it is the system in which Harrison verified the correctness of Intel's floating-point division algorithm after the Pentium FDIV bug.

HOL4.

HOL4 is the more “industrial” member of the family, with strong support for hardware verification, protocol verification, and formal methods in general. Its CakeML project [81] produced a verified ML compiler with end-to-end guarantees from source code to machine code.

Metamath

Metamath, created by Norman Megill in 1992, takes minimalism to its logical extreme [82]. The Metamath language has exactly one inference rule (substitution) and one axiom schema (for propositional calculus). Everything else, including predicate logic, set theory, and all of mathematics, is built up from these primitives.

The set.mm database.

The set.mm database is Metamath's main mathematical library. It formalizes mathematics starting from ZFC set theory and contains over 40,000 proven theorems, including the Cauchy–Schwarz inequality, the fundamental theorem of algebra, and Bertrand's postulate. Every proof in set.mm is a sequence of substitution instances of previously proved theorems, making proofs independently verifiable by trivial checkers.

Relevance to AI.

Metamath's extreme simplicity has made it attractive for early AI experiments in theorem proving. The GPT-f system [83] was originally trained and evaluated on Metamath proofs. The uniform, substitution-based proof format is easy for language models to parse and generate, though the resulting proofs are far more verbose than tactic-based proofs in Lean or Coq.

ACL2

ACL2 (“A Computational Logic for Applicative Common Lisp”) is a theorem prover and programming language developed by Matt Kaufmann and J Strother Moore [84]. It descends from the Boyer–Moore theorem prover (Nqthm) and is based on first-order logic with induction over a Lisp-like language.

Key features.

• Automated induction. ACL2's induction heuristic is legendary: given a recursive function and a conjecture about it, ACL2 can often find the correct induction scheme automatically.

• Industrial adoption. ACL2 has been used extensively at AMD and Intel for microprocessor verification. The verification of the AMD K5 floating-point unit and various Intel designs were carried out in ACL2.

• Executable specifications. Because ACL2 specifications are executable Lisp programs, they can be tested as well as proved. This bridges the gap between testing and verification.

Limitations.

ACL2 is limited to first-order logic and does not support dependent types or higher-order functions. Its Lisp-based syntax is unfamiliar to most mathematicians. The community is small and concentrated in industry.

Detailed Comparison

Table 1 presents a systematic comparison of the major theorem provers across several dimensions relevant to AI-driven formalization.

Why Lean 4 Is Winning

The claim that “Lean 4 is winning” requires immediate qualification: winning for AI-driven formalization, not necessarily winning for all use cases. Isabelle/HOL remains the system of choice for many industrial verification tasks. Coq remains dominant in programming language research. Agda remains the best environment for experimenting with advanced type theory. But for the specific goal of building AI systems that can do mathematics, Lean 4 has emerged as the clear leader. Several factors contribute.

A fast, modern compiler.

Lean 4's compiler generates efficient native code, making it feasible to run large-scale experiments (millions of tactic invocations) in reasonable time. Coq and Isabelle, by contrast, have slower execution environments that bottleneck training loops.

A general-purpose programming language.

Lean 4 is not just a proof assistant but a general-purpose functional programming language. This means that tools for interacting with Lean (parsing output, constructing tactic sequences, managing sessions) can be written in Lean itself, reducing the impedance mismatch between the prover and the AI infrastructure. Projects like LeanDojo exploit this by providing Python bindings that communicate with a Lean server [9].

Mathlib.

Mathlib is the largest coherent library of formalized mathematics in any system. As of 2024, it contains over 170,000 theorems, covers large portions of undergraduate and graduate mathematics, and is growing by hundreds of theorems per week. For AI, a large, well-organized, and actively maintained library is essential: it provides both the training data (theorem statements and proofs) and the infrastructure (lemmas and definitions) that generated proofs can build on.

Microsoft backing.

Lean 4 is developed by Leonardo de Moura's team at Microsoft Research. While Microsoft does not control the Lean community, its funding provides stability and resources (including a team of full-time developers) that volunteer-driven projects cannot match.

AI-friendliness.

Lean 4's design choices are unusually well-suited to AI:

• The tactic mode provides a natural interface for generative models (generate one tactic at a time, observe the resulting proof state, generate the next tactic).

• The metaprogramming framework allows custom interaction modes to be built without modifying the core system.

• The Language Server Protocol (LSP) integration means that AI tools can communicate with Lean through a standard interface.

• The Lean REPL allows programmatic evaluation of expressions and tactics.

Cross-System Proof Transfer

A natural question is whether proofs can be transferred between different theorem provers. If the Four Color Theorem is proved in Coq and the Kepler Conjecture is proved in Isabelle, can we use both results in Lean 4 without re-proving them?

The short answer is: not easily. The obstacles are both foundational and practical.

Foundational obstacles.

Different provers use different logical foundations. Lean 4 and Coq both use the Calculus of Inductive Constructions, but with subtly different universe hierarchies and definitional equalities. Isabelle uses classical higher-order logic, which lacks dependent types but includes the axiom of choice and classical logic from the start. Mizar uses first-order set theory. These differences mean that a statement that is “obvious” in one system may require significant reformulation in another.

Practical obstacles.

Even when the foundations are compatible, the libraries are not. Lean's Mathlib defines real numbers as the completion of the rationals via Cauchy sequences. Coq's standard library uses Dedekind cuts. Isabelle's HOL-Analysis library uses a type class-based approach. Translating between these representations is possible in principle but tedious in practice.

Current approaches.

Several research projects are working on cross-system proof transfer:

• Dedukti is a logical framework based on the $\lambda \mathrm{\Pi }$-calculus modulo rewriting. It can encode the logics of Coq, HOL, and Lean as rewrite systems, enabling (in principle) translation between any two systems via Dedukti as an intermediate representation.

• Statement alignment uses AI (typically embedding-based retrieval) to find corresponding theorems across different libraries. For example, a model might learn that Mathlib's Nat.Prime corresponds to MathComp's prime and Isabelle's prime predicate.

• Proof replay translates tactic-level proofs by mapping tactics in one system to equivalent tactics in another. This is feasible for simple proofs but breaks down when tactics have no counterpart in the target system.

Will there be convergence?

It is tempting to predict that one system will eventually “win” and the others will fade. History suggests otherwise: Coq, Isabelle, and Mizar have coexisted for over three decades. Each system occupies a niche defined by its foundations, its community, and its accumulated library. What is more likely than convergence is interoperation: AI systems that can work with multiple provers, translating between them as needed, just as multilingual NLP systems can work with many languages [85].

Nevertheless, for the specific purpose of training generative models for mathematics, Lean 4 has achieved a critical mass of data (Mathlib), tooling (LeanDojo, REPL), and community momentum that makes it the default choice for new AI research projects as of 2024–2025. We expect this dominance to persist for at least the next several years.

Foundations and Trust

An important dimension of comparison is the size and complexity of the trusted computing base (TCB): the minimal set of code that must be correct for the system's proofs to be trustworthy.

For Lean 4, the TCB consists of the kernel type-checker (approximately 6,000 lines of C++ code in Lean's runtime) plus the axioms of the type theory. Everything else, including tactics, macros, and elaboration, is untrusted: a bug in a tactic can cause an incorrect proof attempt, but it cannot produce a proof that passes the kernel check.

For HOL Light, the TCB is remarkably small: about 400 lines of OCaml. This is possible because HOL's simple type theory has a much simpler kernel than CIC.

For Isabelle, the situation is intermediate: the kernel is larger than HOL Light's but is augmented by the Isabelle/Isar framework, and results proved via Sledgehammer are reconstructed internally.

For Metamath, the TCB is minimal by design: a Metamath proof checker can be implemented in under 300 lines of code in many languages, and dozens of independent implementations exist.

The Role of Libraries

The utility of a theorem prover depends critically on its formal library. A beautiful type theory with an empty library is useless for practical formalization. Table 2 compares the major formal libraries.

The raw numbers are misleading without context. Isabelle's AFP has the most lines of code, but many entries are independent and not organized into a coherent library. Mathlib is monolithic and internally consistent: every definition builds on every other, and the entire library is checked as a single unit. This coherence makes Mathlib uniquely valuable for AI: a model trained on Mathlib can expect that any lemma it invokes will be compatible with any other lemma in the library.

Implications for AI Research

The diversity of theorem provers has important implications for AI research in formalization:

Training data.

Each formal library represents a corpus of human-written proofs in a specific formal language. A model trained exclusively on Mathlib cannot generate Coq proofs (and vice versa), but the underlying mathematical reasoning is the same. This suggests that multilingual models, trained on multiple formal libraries simultaneously, could transfer reasoning skills across systems, much as multilingual language models transfer linguistic knowledge across languages [86].

Evaluation.

Evaluating AI theorem provers is complicated by the diversity of systems. A model that solves 50% of Lean 4 benchmarks and a model that solves 50% of Isabelle benchmarks are not necessarily comparable, because the benchmarks may differ in difficulty, domain, and proof style. Standardized, cross-system benchmarks would be valuable but are hard to construct because of the foundational and library differences discussed above.

Tool integration.

AI tools must interface with the theorem prover's interactive mode. Each prover has its own interface: Lean 4 has the LSP and REPL, Coq has SerAPI and coq-lsp, Isabelle has PIDE (Prover IDE), and HOL Light has an OCaml toplevel. Building infrastructure for AI interaction is a significant engineering effort, and the existence of tools like LeanDojo [9] for Lean 4 and CoqGym [87] for Coq has directly driven the choice of system in many AI papers.

Exercises for Section 7

Theorem add_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m. induction n as [|n' IHn'].
  - simpl. rewrite Nat.add_0_r. reflexivity.
  - simpl. rewrite IHn'. rewrite Nat.add_succ_r. reflexivity.
Qed.

Classical Automated Theorem Proving

The dream of reducing reasoning to computation is older than computers themselves. Long before silicon circuits could evaluate a single Boolean formula, philosophers and mathematicians imagined machines that would settle disputes, verify arguments, and extend the frontiers of knowledge through purely mechanical manipulation of symbols. This section traces that dream from its philosophical origins through the sophisticated automated theorem provers (ATPs) of the early twenty-first century, arriving at a clear picture of what classical methods can and cannot do, and why the arrival of generative models represents a genuine paradigm shift.

Understanding classical ATP is essential for appreciating the contributions of generative models to mathematics. Many of the most successful modern systems combine neural generation with classical verification: the generative model proposes proof steps, and a classical prover checks them. Without understanding the checker, we cannot understand the system.

The Dream of Mechanical Reasoning

In 1666, Gottfried Wilhelm Leibniz, then a twenty-year-old student at the University of Altdorf, published his Dissertatio de Arte Combinatoria, in which he outlined a breathtaking vision: a characteristica universalis, a universal formal language capable of expressing all human thought, and a calculus ratiocinator, a mechanical procedure for deciding the truth or falsity of any statement expressed in that language [88]. When two philosophers disagreed, Leibniz wrote, they would need only sit down together, take up their pens, and say: “Calculemus” (let us calculate).

Leibniz's vision was far ahead of his time, and he never came close to realising it. But the dream persisted. In the nineteenth century, George Boole developed his algebra of logic [89], showing that at least some forms of reasoning could be reduced to algebraic manipulation. Augustus De Morgan formalised the laws that bear his name. Gottlob Frege constructed the first complete system of predicate logic [90].

The dream reached its most precise formulation in 1928, when David Hilbert and Wilhelm Ackermann posed the Entscheidungsproblem (decision problem): is there an algorithm that takes as input a statement in first-order logic and determines, in finitely many steps, whether that statement is universally valid? [91] If such an algorithm existed, it would be Leibniz's calculus ratiocinator made real.

The answer, as we now know, is no. In 1936, Alonzo Church and Alan Turing independently proved that the Entscheidungsproblem is undecidable: no algorithm can decide the validity of all first-order sentences [92][93]. This was a fundamental negative result. But it was not the end of the story. Undecidability means that no single algorithm can solve all instances. It does not mean that clever algorithms cannot solve many instances, and indeed that is precisely what the subsequent eighty years of research have shown.

Resolution-Based Proving

The modern era of automated theorem proving begins with J. Alan Robinson's 1965 paper introducing the resolution principle [22]. Resolution is a single inference rule that, when combined with a systematic search strategy, is refutation complete for first-order logic: if a set of clauses is unsatisfiable, resolution will derive the empty clause (a contradiction) in finitely many steps.

Before describing resolution, we must establish the logical framework in which it operates.

Propositional Logic: SAT Solving

The simplest setting is propositional logic. A propositional formula is built from Boolean variables $x_1,x_2,\dots ,x_n$ using the connectives $\neg$ (not), $\wedge$ (and), $\vee$ (or), $\to$ (implies), and $\leftrightarrow$ (if and only if). The satisfiability problem (SAT) asks: given a propositional formula $\phi$, is there an assignment of truth values to the variables that makes $\phi$ true?

The propositional resolution rule is simple: from two clauses $C_1=A\vee x$ and $C_2=B\vee \neg x$, derive the resolvent $C=A\vee B$. The variable $x$ is resolved upon. If both $A$ and $B$ are empty, the resolvent is the empty clause $\perp$, indicating unsatisfiability.

The DPLL algorithm.

The Davis–Putnam–Logemann–Loveland (DPLL) algorithm, introduced in 1962 [94], is the foundation of all modern SAT solvers. DPLL combines three key ideas:

1. Unit propagation. If a clause contains only one unassigned literal, that literal must be true. Assign it and simplify the formula.

2. Pure literal elimination. If a variable appears only positively (or only negatively) in all remaining clauses, assign it to make all its occurrences true.

3. Branching. Choose an unassigned variable, assign it true, and recurse. If a contradiction is found, backtrack and try false.

DPLL performs a depth-first search over the space of partial assignments, using unit propagation and pure literal elimination to prune the search tree. In the worst case, the search tree has $2^n$ leaves (one for each complete assignment), but in practice the pruning is remarkably effective.

Conflict-driven clause learning.

The major breakthrough that transformed SAT solving from a theoretical curiosity into a practical powerhouse was conflict-driven clause learning (CDCL), developed by Marques-Silva and Sakallah [95] and independently by Bayardo and Schrag [96].

CDCL extends DPLL with two crucial mechanisms:

1. Clause learning. When a conflict is detected (unit propagation derives both $x$ and $\neg x$), the solver analyses the conflict to identify a conflict clause: a new clause that captures the reason for the conflict. This clause is added to the formula, preventing the solver from making the same mistake again.

2. Non-chronological backtracking. Instead of backtracking to the most recent decision (as in DPLL), CDCL jumps back to the earliest decision level that is relevant to the conflict. This can skip many levels of the search tree.

Modern SAT solvers such as MiniSat [97], CaDiCaL [98], and Kissat implement CDCL with numerous additional techniques: variable state independent decaying sum (VSIDS) heuristics for variable selection, restarts to escape unproductive regions of the search space, and inprocessing (simplifying the formula during search).

The practical impact of CDCL is staggering. Industrial SAT instances with millions of variables and clauses are now solved routinely. The annual SAT Competition drives continuous improvements, and SAT solvers underpin everything from hardware verification to planning to cryptanalysis.

First-Order Logic: Unification and Resolution

Propositional logic is limited: it cannot express quantified statements like “for all natural numbers $n$, if $n$ is even then $n^2$ is even.” First-order logic (FOL) adds variables, quantifiers ($\forall$, $\exists$), functions, and predicates, enabling the expression of most mathematical statements.

Resolution in first-order logic requires an additional mechanism: unification. Given two atoms $P(s_1,\dots ,s_k)$ and $P(t_1,\dots ,t_k)$, a unifier is a substitution $\sigma$ such that $P(s_1,\dots ,s_k)\sigma =P(t_1,\dots ,t_k)\sigma$. The most general unifier (MGU) is the unifier that makes the fewest commitments.

First-order resolution then proceeds as follows. Given clauses $C_1=A\vee L_1$ and $C_2=B\vee \neg L_2$, where $L_1$ and $L_2$ can be unified with MGU $\sigma$, derive the resolvent $(A\vee B)\sigma$. Combined with Skolemization (replacing existential quantifiers with Skolem functions) and clausification (converting to clause normal form), resolution is refutation complete for first-order logic.

Paramodulation.

Equality is pervasive in mathematics. The axiom $a=b$ means that $a$ can be replaced by $b$ in any context. Handling equality within resolution requires a special inference rule called paramodulation: from a clause containing $s=t$ and another clause containing a subterm matching $s$, derive a new clause with that subterm replaced by $t$.

Formally, if $C_1=A\vee (s=t)$ and $C_2=B[u]$ where $u$ unifies with $s$ via MGU $\sigma$, then paramodulation derives $(A\vee B[t])\sigma$. Modern provers use ordered paramodulation and superposition calculus to restrict the application of this rule to cases where it is likely to be productive [99].

Major first-order provers.

Three systems dominate the landscape of first-order automated theorem proving:

• Vampire, developed by Voronkov and Kovács [23], has won the most divisions of the annual CASC (CADE ATP System Competition) of any prover. Vampire implements superposition with a sophisticated set of simplification and redundancy elimination techniques.

• E prover, developed by Schulz [24], is an open-source superposition prover known for its flexibility and extensibility. E's clause selection heuristics can be configured through a rich set of parameters, making it a popular platform for machine learning integration.

• SPASS, developed by Weidenbach and colleagues [25], combines superposition with splitting and other inference rules. SPASS has been particularly influential in the development of the superposition calculus.

These provers routinely solve problems in first-order logic with equality that would be far beyond human capacity if approached purely mechanically. They are the workhorses of formal verification, and as we shall see in later sections, they serve as the verification backends for many neural theorem proving systems.

Satisfiability Modulo Theories

Resolution-based provers operate in “pure” first-order logic. But many practical verification and reasoning tasks involve domain-specific operations: arithmetic, arrays, bit vectors, strings. Encoding these operations in raw first-order logic is possible but extremely inefficient. Satisfiability Modulo Theories (SMT) solvers address this by combining a SAT solver with specialised theory solvers that understand the semantics of specific domains [26].

Major SMT Solvers

The three most widely used SMT solvers are:

• Z3, developed at Microsoft Research by de Moura and Bjrner [26], is arguably the most influential SMT solver. Z3 supports a vast array of theories (linear and nonlinear arithmetic over integers and reals, bit vectors, arrays, strings, floating-point arithmetic, algebraic datatypes, sequences, and regular expressions) and has been integrated into hundreds of tools for program analysis, verification, synthesis, and testing.

• CVC5, the latest in the CVC family developed at Stanford and the University of Iowa [27], is Z3's closest competitor. CVC5 excels at quantified formulas and has strong support for strings and regular expressions. It also supports syntax-guided synthesis (SyGuS), where the solver constructs programs that satisfy a given specification.

• Yices, developed at SRI International [28], is known for its efficiency on linear arithmetic and bit-vector problems. Yices was the first solver to win the SMT Competition in all main-track divisions simultaneously.

Theories and Their Applications

The power of SMT comes from the breadth of supported theories. Each theory provides a decision procedure for formulas involving its function symbols, and the DPLL($𝒯$) framework combines these procedures with a Boolean backbone [100].

• Linear arithmetic (${𝒯}_{\text{LIA}}$, ${𝒯}_{\text{LRA}}$): supports $+$, $-$, $<$, $\le$, $=$, and multiplication by constants, over integers (LIA) or reals (LRA). The Simplex algorithm underlies most LRA solvers; LIA adds branch-and-bound or Omega test.

• Arrays (${𝒯}_{\text{Arr}}$) : supports select (read) and store (write) operations. The theory is axiomatised by the read-over-write axiom: $\text{𝚜𝚎𝚕𝚎𝚌𝚝}(\text{𝚜𝚝𝚘𝚛𝚎}(a,i,v),i)=v$ and $i\ne j\Rightarrow \text{𝚜𝚎𝚕𝚎𝚌𝚝}(\text{𝚜𝚝𝚘𝚛𝚎}(a,i,v),j)=\text{𝚜𝚎𝚕𝚎𝚌𝚝}(a,j)$.

• Bit vectors (${𝒯}_{\text{BV}}$) : supports fixed-width binary arithmetic, bitwise operations, shifting, and extraction. Essential for hardware and low-level software verification.

• Uninterpreted functions (${𝒯}_{\text{UF}}$) : the simplest theory, asserting only that equal arguments yield equal results (the congruence axiom). Combined with other theories via the Nelson–Oppen or Shostak combination methods.

SMT solvers have applications far beyond pure mathematics. They are central to:

• Software verification: checking that programs satisfy their specifications (e.g., Dafny [29], Frama-C).

• Bounded model checking: verifying hardware circuits up to a fixed depth.

• Planning: encoding planning problems as SMT formulas.

• Test generation: generating test inputs that cover specific program paths (e.g., KLEE [30]).

• Symbolic execution: exploring program paths with symbolic inputs.

  int abs(int x) {
    if (x >= 0) return x;
    else return -x;
  }

The interaction between the SAT core and the theory solvers is governed by the DPLL($𝒯$) framework [100]. The SAT solver proposes a Boolean assignment to the “theory atoms” (the atomic formulas involving theory symbols). The theory solver then checks whether this assignment is consistent with the theory. If not, the theory solver produces a theory conflict clause that explains why the assignment is inconsistent, and the SAT solver uses this clause to guide its search (exactly as it would use a learned clause in CDCL). This lazy approach avoids the need to eagerly enumerate all theory consequences, and it has proven remarkably effective in practice.

Interactive Theorem Proving with Automation

Automated theorem provers and SMT solvers excel at small, well-defined logical problems. But most real mathematical theorems are far too complex for any ATP to prove from scratch. The proof of the Feit–Thompson theorem (that every finite group of odd order is solvable) spans thousands of pages; the formalisation in Coq required over 170,000 lines of code [16]. For such theorems, human mathematicians (or human formalisers) must provide the overall proof strategy, breaking the proof into lemmas small enough for automation to handle.

This is the domain of interactive theorem provers (ITPs), also called proof assistants: systems in which a human user guides the proof while the machine checks each step and, increasingly, automates the tedious parts. The leading ITPs include:

• Isabelle/HOL: based on higher-order logic, with a rich library (the Archive of Formal Proofs) and powerful automation.

• Coq: based on the Calculus of Inductive Constructions (CIC), with dependent types and a tactic language (Ltac, Ltac2).

• Lean: a newer system with a modern type theory, a growing mathematical library (Mathlib), and strong community engagement.

• HOL Light: a minimalist higher-order logic prover, used for the Flyspeck project (formal verification of the Kepler conjecture) [7].

Sledgehammer: bridging ITPs and ATPs.

The most celebrated bridge between interactive and automated theorem proving is Isabelle's Sledgehammer [65]. Sledgehammer automates the most tedious step of interactive proving: finding which previously proved lemmas are needed and showing that they imply the current goal.

Sledgehammer operates in three phases:

1. Relevance filtering. The Isabelle library contains hundreds of thousands of lemmas. Sending all of them to an ATP would overwhelm it. Sledgehammer uses two complementary filters: itemize

2. MePo (Meng–Paulson filter): a symbol-based heuristic that selects lemmas sharing function and predicate symbols with the current goal.

3. MaSh (Machine Learning for Sledgehammer): a machine learning system that learns from past proofs which lemmas are likely to be useful for goals with similar features [31]. itemize Typically, about 500 relevant facts are selected.

4. ATP invocation. The selected facts and the negated goal are translated into first-order logic (using various encoding strategies for higher-order features) and sent to multiple ATPs (Vampire, E, SPASS) and SMT solvers (Z3, CVC5) in parallel, each with a timeout (typically 30 seconds).

5. Proof reconstruction. If an ATP finds a proof, its output must be translated back into a verified Isabelle proof. Sledgehammer uses metis (a built-in resolution prover) or the smt method to reconstruct the proof within Isabelle's trusted kernel, ensuring that the ATP's result is independently verified.

Sledgehammer's success rate is impressive. On typical Isabelle proof obligations, Sledgehammer can close 40–50% of goals automatically, dramatically reducing the human effort required for formalisation [65].

CoqHammer.

CoqHammer [101] brings similar functionality to the Coq proof assistant. The architecture mirrors Sledgehammer's: relevance filtering selects lemmas from Coq's library, translation converts the goal and lemmas to first-order logic, external ATPs search for proofs, and reconstruction rebuilds the proof within Coq's type-theoretic kernel.

The translation from Coq to first-order logic is more challenging than from Isabelle, because Coq's type theory (the Calculus of Inductive Constructions) is more expressive than Isabelle's higher-order logic. Dependent types, universe polymorphism, and inductive families must all be encoded, and the encoding necessarily loses information. Despite these challenges, CoqHammer achieves success rates of 30–40% on standard Coq proof obligations.

Limitations of Classical ATP

Classical automated theorem provers are among the great achievements of computer science. They are sound, they are (semi-)complete, and they can solve problems that would take humans years. Yet they have fundamental limitations that motivate the search for new approaches.

No mathematical understanding.

A resolution prover does not “understand” mathematics. It manipulates symbols according to inference rules, without any concept of what those symbols mean. It cannot look at a formula and think, “This looks like it should follow from the intermediate value theorem.” It cannot recognise that a proof is “elegant” or “natural.” It cannot draw an analogy between two different areas of mathematics.

Combinatorial explosion.

The search space of resolution grows exponentially with the number of clauses and the depth of terms. For problems in domains like group theory, ring theory, or combinatorics, the number of possible inferences at each step is enormous, and most branches of the search tree lead nowhere. Heuristics help, but they cannot eliminate the fundamental exponential nature of the search.

No concept discovery.

Perhaps the most fundamental limitation is that classical ATPs cannot discover new concepts. A prover can only work with the concepts that are already present in the axioms and the goal. It cannot invent a new definition, introduce an auxiliary construction, or reformulate a problem in a more tractable form. Yet concept discovery is at the heart of mathematical creativity.

The knowledge bottleneck.

An ATP has access only to the axioms and lemmas it is given. In contrast, a human mathematician draws on a vast background of mathematical knowledge: techniques from analysis applied to number theory, topological arguments in algebra, probabilistic methods in combinatorics. This cross-pollination of ideas is central to mathematical progress, and classical ATPs have no mechanism for it.

Inability to handle informal reasoning.

The vast majority of mathematical communication occurs in natural language, supplemented by formal notation. Textbooks, research papers, lectures, and mathematical conversations all use a blend of rigour and informality that is inaccessible to classical ATPs. When a mathematician says “by a standard compactness argument,” a human reader understands what this means and can fill in the details. An ATP has no mechanism for interpreting such informal guidance.

The Mathematical Reasoning Landscape Before LLMs

By 2019, the landscape of machine-assisted mathematical reasoning was fragmented into distinct traditions, each powerful in its own domain but fundamentally limited. Computer algebra systems could compute but not prove. Automated theorem provers could prove but not understand. Interactive theorem provers required painstaking human guidance. And a nascent wave of neural approaches was beginning to show that machine learning could contribute to theorem proving, though the contributions were still modest.

This section surveys the state of affairs before the transformative impact of large language models, identifying both the achievements and the gaps that LLMs would later begin to fill. Understanding this landscape is essential for appreciating why the arrival of LLMs was such a significant event in the history of mathematical reasoning.

Computer Algebra Systems: Computation Without Proof

Computer algebra systems (CAS) are among the oldest and most successful tools for machine-assisted mathematics. Systems like Mathematica [102], Maple, SageMath [103], and SymPy [104] can perform symbolic differentiation and integration, solve equations, factor polynomials, compute limits, manipulate matrices, and carry out hundreds of other algebraic operations with speed and reliability that far exceeds human capability.

The key distinction, however, is between computation and proof. A CAS can compute that ${\int }_0^1{x}^{2}dx=1/3$, but it does not produce a proof of this fact in any formal sense. It applies algorithms (Risch integration, Gröbner basis computation, etc.) that are known to be correct, but the correctness of the implementation is trusted, not verified.

The gulf between CAS and ITP is not merely a matter of software engineering. It reflects a deep conceptual distinction between knowing the answer and knowing why the answer is correct. A CAS computes answers using algorithms whose correctness has been proved by humans (in informal mathematics, published in journals). An ITP verifies every step against a small, trusted logical kernel. The CAS approach is efficient but relies on trust in complex software; the ITP approach is rigorous but painfully slow. Bridging this gap is one of the great promises of generative models.

The IMO Grand Challenge

In 2019, a group of researchers including Daniel Selsam (Microsoft Research), Kevin Buzzard (Imperial College London), and others issued the IMO Grand Challenge: to build an AI system capable of winning a gold medal at the International Mathematical Olympiad (IMO) [105].

The IMO is the most prestigious mathematical competition for pre-university students. Each year, roughly 600 contestants from over 100 countries solve six problems in two sessions of 4.5 hours each. The problems span algebra, combinatorics, geometry, and number theory, and they require deep mathematical insight, creative problem-solving, and rigorous proof construction. A gold medal typically requires solving four or more of the six problems.

The IMO Grand Challenge specifies two crucial requirements:

1. Formal proofs. The system must produce proofs that can be verified by a formal proof checker. Natural language arguments, no matter how convincing, do not count. This ensures that the system has genuinely “proved” its answers, not merely guessed them.

2. Time limit. The system must work within the same time constraints as human contestants: 4.5 hours per session of three problems.

As of 2019, no AI system came close to this goal. The best automated systems could handle only the simplest competition problems, and even then required significant human assistance in formalisation. The challenge crystallised the gap between the state of the art in AI and the level of mathematical reasoning that talented human teenagers achieve routinely.

The IMO Grand Challenge served as a rallying point for the mathematical AI community. It made concrete what had previously been vague aspirations, and it set a standard against which progress could be measured. When DeepMind's AlphaProof system solved several IMO problems in 2024 (a development we discuss in later sections), the community could point to the IMO Grand Challenge as the benchmark that defined the goal.

Early Neural Approaches to Theorem Proving

The period from 2016 to 2020 saw a burst of activity in applying neural networks to theorem proving. These early efforts were modest in scope compared to what would come later, but they established many of the key ideas and architectures that subsequent work would build upon.

DeepMath: Predicting Premise Relevance

The first major application of deep learning to theorem proving was DeepMath, published by Alemi, Chollet, Irving, Szegedy, and Urban in 2016 [106].

DeepMath addressed a specific subproblem: premise selection. Given a conjecture to be proved, which of the thousands of available lemmas in the library are most likely to be useful? This is the same problem that Sledgehammer's MaSh filter addresses, but DeepMath tackled it with deep neural networks rather than hand-crafted features.

DeepMath trained convolutional neural networks (CNNs) and recurrent neural networks on the Mizar Mathematical Library, learning to predict whether a given premise was used in the proof of a given theorem. The results were encouraging: DeepMath's premise selection, when combined with the E prover, proved 7.36% of held-out Mizar theorems, compared to 4.98% for E with its default heuristics.

The DeepMath approach highlighted a recurring theme: the bottleneck in automated theorem proving is often not the proving itself but the selection of relevant information. A library of 50,000 theorems contains a vast amount of useful knowledge, but presenting all of it to a prover is counterproductive. The prover drowns in irrelevant information and wastes its search budget exploring dead ends. Neural premise selection provides a principled way to filter this information, and subsequent work would refine this idea considerably.

GamePad: Learning to Prove in Coq

In 2018, Huang, Dhariwal, Song, and Li [107] introduced GamePad, a system for learning to prove theorems in Coq.

GamePad framed theorem proving as a game: the “state” is the current proof goal (a formula to be proved, along with the available hypotheses), and the “actions” are the tactics that can be applied. A neural network, trained on a dataset of human-written Coq proofs, learned to predict which tactic to apply given the current goal.

The key technical contribution of GamePad was its representation of proof states. Coq proof goals are abstract syntax trees (ASTs) that can be very deep and complex. GamePad used tree-structured neural networks to encode these ASTs into fixed-dimensional vectors, enabling the neural network to reason about the structure of mathematical expressions.

GamePad demonstrated proof automation on the Feit–Thompson formalisation, one of the most complex formalisations in Coq. While the results were preliminary (GamePad could close only a small fraction of goals), the approach showed that neural networks could learn meaningful representations of formal mathematical objects.

HOList: Learning Theorem Proving in HOL Light

In 2019, Bansal, Loos, Rabe, Szegedy, and Wilcox [108] introduced HOList, a benchmark and learning environment for theorem proving in HOL Light.

HOList made several important contributions:

1. A large-scale benchmark. HOList extracted over 29,000 theorems from the core HOL Light library, along with their proofs, creating the largest benchmark for neural theorem proving at the time.

2. A reinforcement learning environment. HOList provided an API for interacting with HOL Light, enabling agents to attempt proofs, receive feedback (success or failure), and learn from experience.

3. Strong baselines. HOList demonstrated that a neural network trained to predict proof steps could, combined with beam search, prove 55.7% of held-out theorems, a substantial improvement over hand-coded heuristics.

GPT-f: Generative Language Models for Formal Proof

The most consequential pre-LLM neural theorem proving system was GPT-f, introduced by Polu and Sutskever in 2020 [2].

GPT-f represented a fundamental shift in how neural networks were applied to theorem proving. Where previous systems (DeepMath, GamePad, HOList) used neural networks to classify or select from a fixed set of actions, GPT-f used a generative language model to generate proof steps as text. The model was a Transformer decoder (based on the GPT architecture) trained on a dataset of formal proofs from the Metamath library.

The results were striking. GPT-f, combined with best-first search, proved 56.22% of held-out Metamath theorems and found 23 new proofs that were shorter than the existing human-written proofs. These new proofs were accepted into the Metamath library, marking the first time that an AI system contributed original proofs to a major mathematical library.

The key architectural innovation of GPT-f was the treatment of proof steps as sequences of tokens rather than as structured objects. By encoding both the proof state and the proof step as strings, GPT-f could leverage the full power of the Transformer architecture, including its ability to capture long-range dependencies and its scalability to large datasets. This flattening of structure was initially controversial (one might expect that preserving the tree structure of mathematical expressions would be beneficial), but the results spoke for themselves.

The Paradigm Shift: From Search to Generation

The progression from DeepMath to GPT-f reveals a fundamental paradigm shift in how neural networks interact with theorem provers.

1. DeepMath (2016): The neural network is a filter: it selects premises from a fixed library, then hands the problem to a classical prover. The prover still does all the reasoning.

2. GamePad/HOList (2018–2019): The neural network is a policy: it selects tactics from a fixed set of options. The prover still executes the tactics, but the neural network guides the search.

3. GPT-f (2020): The neural network is a generator: it produces proof steps as text, drawing on its training to construct novel tactic invocations with appropriate arguments. The prover becomes a verifier, checking the generated steps rather than producing them.

This shift from search-based to generation-based proving has profound implications. In the search paradigm, the prover explores a combinatorial space defined by the inference rules. In the generation paradigm, the model draws on learned patterns to propose proof steps directly, bypassing much of the combinatorial search. The trade-off is that the generated steps may be incorrect (the model “hallucinates”), but the formal verification kernel catches all errors.

What Was Missing Before LLMs

Despite the progress of 2016–2020, several critical capabilities were missing from the pre-LLM landscape:

Broad mathematical knowledge.

Pre-LLM neural theorem provers were trained on specific formal libraries (Mizar, HOL Light, Metamath). They learned the patterns within those libraries, but they had no access to the vast informal mathematical knowledge contained in textbooks, research papers, lecture notes, and online forums. A system trained on Metamath's library of 38,000 theorems has a very different knowledge base from a mathematician who has read hundreds of papers across multiple subfields.

Natural language understanding.

Mathematical reasoning is conducted largely in natural language, supplemented by formal notation. A mathematician reading a proof switches fluidly between English (or French, or any other natural language) and symbols. Pre-LLM systems operated entirely in the formal language of their proof assistant, with no ability to understand or produce natural language mathematics.

Proof sketching.

Human mathematicians typically work by first constructing a proof sketch: a high-level outline that captures the key ideas without filling in all the details. They then refine the sketch, adding rigour where needed. Pre-LLM systems had no mechanism for this kind of hierarchical planning. They generated proofs one step at a time, with no ability to “step back” and consider the overall proof strategy.

Autoformalization.

The vast majority of mathematics is written in natural language, not in formal logic. Autoformalization, the task of automatically translating natural language mathematics into formal specifications, was essentially unsolved before LLMs. This created a bottleneck: even if a prover could find a proof once the problem was formalised, the formalisation step itself required expert human effort.

Cross-domain transfer.

Some of the most beautiful proofs in mathematics draw on unexpected connections between different areas. Erdos's probabilistic method uses probability theory to prove combinatorial results. The proof of Fermat's Last Theorem connects number theory, algebraic geometry, and the theory of modular forms. Pre-LLM theorem provers, trained on a single formal library, had no mechanism for this kind of cross-domain transfer. They could not “borrow” a technique from analysis to prove a result in combinatorics, because they had no understanding of the analogies that make such borrowing possible.

Informal-to-formal translation.

The gap between informal and formal mathematics is vast. Consider the statement: “A continuous function on a closed interval attains its maximum.” A human mathematician instantly understands this as the extreme value theorem. Translating it into a formal statement requires specifying the types (real-valued function on $[a,b]$), the topology (the standard topology on $ℝ$), the definition of continuity ($ϵ$-$\delta$ or via open sets), and the definition of “attains” ($\exists c\in [a,b],f(c)=\sup \{f(x):x\in [a,b]\}$). Before LLMs, this translation was a manual process requiring expertise in both mathematics and the target proof assistant.

The Role of Search in Theorem Proving

Whether the proof steps are generated by classical inference rules or by neural networks, the fundamental computational structure of theorem proving is search. The proof state defines a tree (or, more generally, a directed acyclic graph) in which each node is a proof state and each edge is a proof step. The root is the initial goal, and the leaves are either closed goals (success) or dead ends (failure). The prover must find a path from the root to a state in which all goals are closed.

Three search algorithms have proven particularly effective for neural theorem proving:

Best-first search.

In best-first search, the prover maintains a priority queue of unexplored proof states, ranked by a value function $V(s)$ that estimates the probability that a proof can be found from state $s$. At each step, the highest-valued state is expanded. When the value function is provided by a neural network, this approach combines the neural network's “intuition” about which states are promising with a systematic exploration strategy.

(BEST First)$$\begin{array}{ccc}& s^{\ast }={\mathrm{arg\hspace{0.17em}max}}_{s\in \text{Frontier}}{V}_{\theta }(s),& \text{<span class="tml-eqn"></span>}\end{array}$$ where $\text{Frontier}$ is the set of unexpanded states and $V_{\theta }$ is a learned value function.

Monte Carlo Tree Search.

MCTS, made famous by its role in AlphaGo, adapts naturally to theorem proving. MCTS balances exploration (trying new proof steps) with exploitation (pursuing promising directions) using the UCB (Upper Confidence Bound) formula: (UCB)$$\begin{array}{ccc}& \text{UCB}(s,a)=\frac{W(s,a)}{N(s,a)}+c\sqrt{\frac{\ln N(s)}{N(s,a)}},& \text{<span class="tml-eqn"></span>}\end{array}$$ where $W(s,a)$ is the cumulative value of taking action $a$ from state $s$, $N(s,a)$ is the number of times action $a$ has been tried from state $s$, $N(s)={\sum }_{a}N(s,a)$, and $c$ is an exploration constant.

MCTS for theorem proving operates in four phases:

1. Selection. Starting from the root, use the UCB formula to select actions until reaching an unexpanded node.

2. Expansion. Apply the neural policy to generate candidate proof steps at the unexpanded node.

3. Simulation/Evaluation. Use the value network to estimate the probability of success from the new state.

4. Backpropagation. Update the visit counts and value estimates along the path from the new node back to the root.

Expert iteration.

Expert iteration, introduced by Anthony, Tian, and Barber [109], is a reinforcement learning framework that alternates between two phases:

1. Search (expert). Use MCTS (or another search algorithm) with the current policy to find proofs. The search acts as an “expert” that is stronger than the raw policy because it explores multiple possibilities.

2. Learning (apprentice). Train the policy network on the proof trajectories found by the search, so that the policy learns to imitate the expert.

The key insight is that the search (expert) is always better than the raw policy (apprentice), because the search explores multiple branches. By training the policy to imitate the search, the policy improves. Then the improved policy makes the search stronger (because the search uses the policy as a prior), which generates even better training data, and so on. This creates a virtuous cycle of self-improvement.

(Expert ITER)$$\begin{array}{ccc}& {\theta }_{k+1}={\mathrm{arg\hspace{0.17em}min}}_{\theta }\sum _{(s,a)\in {𝒟}_k}ℒ({\pi }_{\theta }(a|s),{\pi }_{\text{MCTS}}(a|s;{\theta }_k)),& \text{<span class="tml-eqn"></span>}\end{array}$$ where ${𝒟}_k$ is the dataset of (state, action) pairs collected by MCTS in iteration $k$, ${\pi }_{\theta }$ is the neural policy, and ${\pi }_{\text{MCTS}}(\cdot ;{\theta }_k)$ is the improved policy from MCTS using ${\pi }_{{\theta }_k}$ as the prior.

Pre-LLM Neural Theorem Proving: A Comparison

To consolidate our understanding of the pre-LLM neural theorem proving landscape, we present a systematic comparison of the major systems.

Several trends emerge from this comparison:

1. Increasing neural autonomy. The role of the neural network evolved from a passive filter (DeepMath) to an active generator (GPT-f). Each successive system gave the neural network more responsibility for the creative work of proof construction.

2. Architectural convergence. Early systems used specialised architectures (CNNs for token sequences, tree-structured RNNs for ASTs, graph neural networks for formula structure). By 2020, the Transformer had become dominant, thanks to its ability to handle variable-length inputs and its scalability.

3. Growing scale. Training datasets grew from thousands of examples (DeepMath) to tens of thousands (HOList, GPT-f). Model sizes grew correspondingly, though they remained small by the standards of the LLM era that was about to begin.

4. Persistent verification. Across all systems, the formal verification kernel remained the final arbiter of correctness. This principle – that the neural network proposes and the kernel verifies – would persist into the LLM era and remains a cornerstone of neural theorem proving.