Learned Theorem Proving: Search, Formalization, and Discovery

A formal checker can evaluate whether a proposed derivation follows its rules without explaining how to find that derivation. Learned theorem proving uses statistical models to guide the search.

The combination is significant because prediction and acceptance perform different jobs. A model can propose an unpromising or invalid step; the formal environment can reject it. Successful search then produces evidence whose validity need not depend on believing the model's explanation.

This account still leaves several questions open: whether the formal statement is faithful, which assumptions the proof uses, how much human assistance shaped the task, and whether the mathematical result was already known.

Learning before large language models

Large formal libraries create a selection problem. A prover may have thousands of available lemmas, while only a small portion is useful for the current goal.

Josef Urban's MaLARea work, beginning in 2007, combined learning with automated reasoning in large theories. Later work with Cezary Kaliszyk, Jiří Vyskočil, and other collaborators developed the interaction further.

Successful proofs supplied information about which premises tend to be useful. A learned selection method could then focus subsequent proof attempts. The original MaLARea paper and later system account document this feedback between deductive search and learned guidance.

Research on premise selection, tactic prediction, and guidance inside first-order provers therefore predates the recent prominence of language models. The newer systems extend a longer history of using experience to improve proof search.

Several tasks under one name

Success at one task does not establish success at all the others.

In particular, finding a proof of a supplied formal theorem avoids part of the translation problem. Translating a theorem into a formal language can be useful even when its proof still requires substantial human work.

A checked search loop

Suppose the goal is $P\land Q\to Q\land P$.

A model proposes introducing the implication's hypothesis. The proof state now contains $h:P\land Q$ and the goal $Q\land P$.

It proposes splitting the conjunction goal. The checker requires evidence for both $Q$ and $P$. Projection from $h$ supplies each component, and the resulting proof term can be checked.

An invalid proposal, such as using $h$ directly as evidence for an unrelated proposition $R$, fails unless the context actually provides a permitted derivation.

For substantial mathematics, the choice of useful intermediate lemmas and representations is much harder. The example nevertheless explains the architecture: the model guides construction; the logical environment determines whether the proposed evidence is acceptable.

Rewriting, normalization, induction, arithmetic procedures, external provers, and learned search can all participate. Modern proof automation is not reducible to SAT or to a single neural mechanism.

AlphaProof as a dated case study

Google DeepMind's 2024 IMO report described a combined result from AlphaProof and the separate AlphaGeometry 2 system. AlphaProof solved three non-geometry problems; AlphaGeometry 2 solved one geometry problem.

The combined score was equivalent to a silver-medal performance. The problems were manually formalized for the systems, and some solutions required computation lasting up to three days, unlike the contestants' timed sessions. These conditions are stated in the July 2024 report.

The methodology paper, “Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning”, was published online in November 2025. It describes training on autoformalized problems, interaction with a Lean environment, and test-time reinforcement learning using related problem variants.

The case demonstrates substantial progress in finding formally checked competition proofs. Its documented conditions do not support a claim of fully autonomous research mathematics under ordinary human time limits.

The report is a historical case study, not a declaration that it remains the latest performance benchmark. Fast-changing comparisons require their own dates and evaluation conditions.

When the theorem is mistranslated

Consider the informal assertion:

“For every real number $x$, there is a real number $y$ greater than $x$.”

Its formal structure is

Choosing $y=x+1$ gives a straightforward proof.

Now suppose a translation accidentally changes the quantifiers:

This claims a real number larger than every real number and is false.

A different mistranslation might weaken the statement to “there exist $x$ and $y$ with $x<y$.” That version is easily proved but does not answer the intended question.

A kernel checks the formula it receives. It does not compare that formula with the author's unstated intention. A high proof-success rate on automatically translated statements therefore needs an accompanying account of translation quality.

A research formalization with an explicit hypothesis

The 2026 PrimeGapsLib project provides a useful example beyond competition problems. The project presentation describes a collaborative formalization of arguments from Maynard and Polymath8b, using a human-developed blueprint, AxiomProver-generated Lean proofs, and subsequent code curation.

For historical accuracy, the scope must be read from the formal artifact.

At commit 1faa7b14e82ddebc2772dfb9153922f01b106477, inspected on 5 September 2026, the main bounded-gap file explicitly takes the Bombieri–Vinogradov proposition as a hypothesis. It derives that consecutive prime gaps are at most 246 infinitely often.

The separate Bombieri–Vinogradov file defines the proposition and carries it through the development as an assumption. The repository's README at that version states the conditional scope as well.

This is a substantial formalization of a known argument under an explicit mathematical hypothesis. The source inspection reported here is not an independent local rebuild of the entire library.

Bombieri–Vinogradov is an established theorem of number theory; treating its formal statement as a supplied hypothesis is nevertheless different from including its formal proof among the checked dependencies. The distinction concerns the completeness of the formal development.

The bound 246 also belongs to earlier mathematical work, following Zhang's breakthrough, Maynard's method, and the Polymath8b collaboration. Formalizing that result with learned assistance does not make the bound itself a new discovery in 2026.

What an audit should establish

An informative report connects five stages:

1. The intended informal statement and its mathematical context.
2. The exact formal statement, including definitions and hypotheses.
3. The method used to find the proof and the human contributions.
4. The checking process, admitted axioms, and external computational dependencies.
5. A versioned artifact that permits examination or reproduction.

These stages answer different questions. A dependency report can expose an additional axiom but cannot determine whether a definition is a good translation. A successful build can establish that the development meets its configured checking rules while still containing explicitly admitted assumptions.

Reproducibility also requires matching library and toolchain versions. A proof script depends on its environment, even when its underlying mathematical theorem is stable.

Evaluating progress

Benchmark comparisons should state the available library, permitted tools, computation budget, and treatment of human assistance.

Training contamination and close variants matter when the intended claim concerns generalization. Reconstructing a familiar proof can be valuable automation while providing different evidence from solving a genuinely new problem.

For mathematical discovery, correctness is only one part of the judgment. A conjecture may be true but already known, trivial under the definitions, or uninteresting for the intended research question.

The historical continuity is clear. Earlier automated provers already separated search from checking, and earlier formalization projects already depended on careful statement design. Learned systems change the power and cost of proposing mathematical steps while inheriting those established obligations.

Returning to the series

The modern history followed here connects several developments: calculi for reasoning, explicit foundations, metatheorems about proof and meaning, theories of computation, and tools for producing and checking formal evidence.

None of these developments eliminates the others. A learned prover still works within a logic; a checker still implements a foundation; a library still depends on mathematical definitions; and an accepted derivation still needs an intelligible interpretation.

Return to the series map to revisit a branch in greater depth, or explore the earlier traditions that developed other systematic accounts of inference and argument.

Sources and further reading

• Josef Urban, “MaLARea: A Metasystem for Automated Reasoning in Large Theories” (2007).
• Jesse Alama and collaborators, “Premise Selection for Mathematics by Corpus Analysis and Kernel Methods” (2011 preprint).
• Cezary Kaliszyk and Josef Urban, “Learning-Assisted Automated Reasoning with Flyspeck” (2012 preprint).
• Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil, “Machine Learner for Automated Reasoning 0.4 and 0.5” (2014).
• Google DeepMind, 2024 IMO report (25 July 2024, subsequently updated).
• Thomas Hubert and collaborators, “Olympiad-Level Formal Mathematical Reasoning with Reinforcement Learning” (online publication, 12 November 2025).
• Axiom Math and collaborators, PrimeGapsLib project and versioned repository (2026).