HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

ArXiv: 1904.03241

🎯 Pitch

A deep learning prover operating directly at HOL Light's tactic level, reinforced on its own proof attempts, matches or beats sophisticated first-order hammers on many theorems without a single logical kernel call. Yet its gains abruptly plateau—the hardest formalized analysis proofs remain out of reach, revealing a stark ceiling tied to tactic expressiveness rather than search scale.

1. Executive Summary

This paper introduces an open-source reinforcement learning environment and benchmark for higher-order theorem proving built on the HOL Light interactive theorem prover, alongside a deep learning driven automated prover called DeepHOL. The system decomposes theorem proving into two learned subtasks—tactic selection and premise argument ranking—via a two-tower WaveNet architecture, and then improves through a distributed reinforcement learning loop that continuously mixes freshly generated proofs with historical examples. On the complex analysis corpus, DeepHOL closes 38.9% of validation theorems in the best loop configuration, substantially surpassing a trivial baseline that calls HOL Light's built-in first-order prover (9.2%) and a purely supervised WaveNet model (31.72%), establishing that reinforcement learning from self-generated proof traces meaningfully improves over imitation learning alone—while also showing that the system remains bounded to proofs within the scope of the available tactic and premise libraries, as the hardest theorems in the Flyspeck formalization yield lower closure rates (37.0%).

2. Context and Motivation

The Core Problem: Making Higher-Order Theorem Proving Accessible to Machine Learning

The fundamental problem this paper tackles is the absence of a standardized, machine learning-friendly environment for automated reasoning in higher-order logic. This is not merely an engineering gap—it represents a structural barrier that has prevented the broader ML community from engaging with one of the most intellectually significant challenges in AI: the formalization and automated discovery of mathematical proofs.

To understand why this gap exists, we need to unpack what "higher-order theorem proving" means and why it is distinct from the first-order logic problems that dominate the existing automated theorem proving (ATP) literature. In first-order logic, quantifiers range only over individual objects (e.g., "for all numbers x, x + 0 = x"). In higher-order logic, quantifiers can range over functions and predicates as well (e.g., "for all functions f, f(0) = 0 if f is linear"). This additional expressive power makes higher-order logic capable of formalizing virtually all of modern mathematics—topology, real analysis, algebraic geometry—in a way that first-order logic simply cannot. But it also makes proof search dramatically harder, because the search space of possible instantiations for higher-order variables is vastly larger and less structured.

The interactive theorem provers (ITPs) that work in higher-order logic—systems like HOL Light, Coq, Isabelle, and Lean—have achieved remarkable results. The formal proof of the Kepler conjecture in HOL Light, for instance, was a 20-person-year effort that required formalizing substantial portions of arithmetic, linear algebra, and multivariate analysis. But these systems demand enormous human expertise. A human user must understand not only the mathematics but also the particular tactic language, the library of already-proved theorems, and the often-baroque conventions of the prover. This expertise bottleneck means that formalization efforts remain rare, expensive, and slow.

The promise of machine learning for ITPs is therefore twofold. First, an ML-driven prover could automate the routine steps of proof construction that currently require human intervention, dramatically accelerating formalization efforts. Second, the act of learning to prove theorems could serve as a testbed for deep reasoning capabilities in AI systems—capabilities that, if achieved, would transfer to scientific reasoning, program verification, and any domain requiring rigorous multi-step inference from formal premises. The paper frames this explicitly in its opening paragraph:

"Formalization of mathematics and the automated creation of new mathematical content is at the frontier of current AI techniques. Given the fundamental nature of mathematics and its importance for most scientific disciplines, the capability for high level formal mathematical reasoning is both an important practical task as well as one of the most challenging case studies in AI."

The Ecosystem Problem: Why ML Researchers Couldn't Meaningfully Attack This Task

The gap the paper addresses is not that no one had tried applying ML to theorem proving—the Related Work section (Section 2) catalogs nearly two decades of such efforts. Rather, the gap is that the field lacked what other ML subfields take for granted: a standardized benchmark, a stable evaluation protocol, and an environment that abstracts away the idiosyncrasies of the underlying prover.

The authors draw an explicit parallel to the transformative role of benchmarks in other ML domains:

"Well-defined, large-scale benchmarks were instrumental for unifying disparate efforts in machine learning research: LibriSpeech for speech recognition, the Netflix prize for recommendation, ImageNet for object recognition, MSCOCO for object detection and segmentation, WMT for machine translation, and SQuAD for question answering—just to name a couple of examples. Benchmarks have fostered collaboration and competition and provide a means to measure progress, contributing significantly to accelerated progress and reproducible science."

The theorem proving community, in contrast, was fragmented across multiple incompatible ITP systems, each with its own logical foundations, tactic languages, and proof representation formats. There was no equivalent of ImageNet for higher-order reasoning—no single dataset and evaluation protocol that allowed researchers to compare different ML approaches on equal footing and track progress over time. This fragmentation meant that ML researchers who wanted to work on theorem proving had to first become experts in a particular ITP system, a barrier that excluded all but a handful of specialists.

The paper's diagnosis of the ecosystem problem extends beyond mere inconvenience. Without a shared benchmark, the field could not distinguish between genuine methodological advances and artifacts of particular experimental setups. Were the results in [19] (which used deep neural networks for premise selection on the Mizar library) better or worse than those in [23] (which used deep networks to guide the ATP E)? There was no way to know, because they operated on different proving systems with different theorem corpora and different evaluation metrics. The field was accumulating results without building cumulative knowledge.

Prior Approaches and Where They Fall Short

The paper's Related Work section (Section 2) provides a detailed accounting of existing approaches, each of which the authors see as addressing part of the problem while leaving critical gaps.

TacticToe (Gauthier et al., 2017) [9]. This is identified as "the first published result on machine learning tackling higher-order theorem proving at a relatively large scale at tactic level." TacticToe uses traditional machine learning (k-nearest neighbors on hand-engineered features) rather than deep learning, and operates within the HOL4 system. The paper gives it qualified praise—"a great success that came with significant improvements over previous automated theorem proving systems"—but identifies two critical limitations. First, it does "not propose an easy to use benchmark or environment for machine learning researchers." The system is deeply embedded in HOL4's OCaml implementation, making it inaccessible to researchers who work primarily in Python and TensorFlow. Second, HOL4 has "significantly less theorems with more complex human proof scripts with a larger number of more elementary tactics," meaning TacticToe operates on a smaller corpus with a different (and arguably harder) action space. This makes TacticToe's approach—relying on nearest-neighbor retrieval of similar proof states—potentially less scalable to the larger theorem libraries that are the whole point of higher-order formalization.

GamePad (Huang et al., 2018) [10]. GamePad is the closest prior work in spirit—the authors explicitly note it has "very similar objectives to ours." GamePad provides a Python API for the Coq interactive theorem prover and defines training and test sets. However, the paper identifies a fundamental scale limitation:

"While enabling automatic code extraction, it comes with a much smaller coverage of fundamental mathematics. Even including the formalization of the Feit-Thompson theorem, their benchmark comprises only 1602 theorems and lemmas, while ours features 29462 theorems and lemmas."

This 18× difference in corpus size is not merely quantitative. A corpus of 1602 theorems is large enough to train a model but not large enough to capture the diversity of reasoning patterns that characterize real mathematical practice. The HOList corpus, derived from the Flyspeck formalization of the Kepler conjecture, includes theorems spanning arithmetic, linear algebra, real analysis, measure theory, and geometric reasoning—a breadth that forces any ML prover to learn genuinely general reasoning strategies rather than overfitting to a narrow domain.

More subtly, the paper notes that GamePad reports "proxy metrics" rather than end-to-end theorem proving performance. This is a crucial methodological distinction. Reporting that a model achieves 85% accuracy at predicting the next tactic in a human proof script tells you something about imitation learning, but it does not tell you whether the model can actually construct proofs from scratch, which requires dealing with compounding errors, exploring branches that humans never took, and recovering from dead ends. The paper positions itself as providing both proxy metrics (tactic prediction accuracy, argument selection error rate) and end-to-end proof closure rates, with the latter being the primary benchmark.

HOLStep (Kaliszyk et al., 2017) [24]. This is perhaps the most directly related prior benchmark effort, as it also derives from the HOL Light corpus. The paper describes it as featuring "a few static datasets" and notes critically that "it remains unclear how performance of machine learning models on this dataset relates to real world prover performance." The issue is that HOLStep is a static classification task—given a proof state and a theorem, predict whether that theorem is a useful premise—without any mechanism for using those predictions to actually construct proofs. There is no search, no feedback loop, no way to observe how errors in premise selection cascade into overall proof failure. The paper's environment, by contrast, provides a full interactive loop where models must live with the consequences of their predictions.

Pure deep reinforcement learning for theorem proving (Whalen, 2016) [21]. The Holophrasm system attempted to learn theorem proving end-to-end via deep RL in the Metamath prover. The paper's assessment is blunt:

"This work was moderately successful, finding mostly proofs for very simple theorems, especially in propositional logic. On the other hand, Metamath is not considered to be a serious contender for large scale mathematical formalization work."

This highlights a tension that runs through the paper's entire framing: it is relatively easy to build an ML prover for a toy logic (Metamath's formalism is simpler than higher-order logic), but the whole point of higher-order theorem proving is to handle the complexity of real mathematics. A system that succeeds only on propositional tautologies is solving a different problem entirely.

First-order ATP with ML premise selection (multiple works). A substantial body of prior work—including [17, 18, 19, 23]—applies machine learning to premise selection for first-order automated theorem provers. The typical architecture is: given a conjecture, use an ML model to rank which previously-proved theorems are most likely to be useful, then call a first-order ATP like E [20] with those theorems as axioms. This approach has been successful enough that it is the dominant paradigm in the field. However, the paper identifies two limitations. First, these systems are "in contrast to our work, [using] neither deep learning nor reinforcement learning" in several cases, though [19] and [23] do use deep learning. Second and more fundamentally, first-order ATPs are the wrong target: higher-order logic is strictly more expressive, and translating higher-order problems to first-order logic (as [17] does) loses information and introduces artifacts. The paper's ambition is to build a prover that operates natively at the higher-order level, making decisions at the same granularity (tactic-level) that human users do.

Non-deep ML for theorem proving (extensive list, references [28–44]). The paper acknowledges a rich tradition of applying traditional machine learning methods to theorem proving—kernel methods, random forests, k-nearest neighbors, naive Bayes—spanning from early work on search control [28] through premise selection for Mizar [13], HOL Light [18], and Isabelle [44]. These works established the viability of learning from proof corpora but are fundamentally limited by their reliance on hand-engineered features and their inability to learn representations from raw proof state syntax. The paper does not belabor this point, but the implication is clear: the field is ready for a transition from feature-engineered ML to deep learning, and that transition requires exactly the kind of standardized environment and benchmark that HOList provides.

What Makes Higher-Order Theorem Proving a Distinct and Harder Problem

To appreciate why the paper's choice of HOL Light matters, we need to understand what distinguishes higher-order logic from the first-order settings that dominate prior ATP work. The paper does not provide a tutorial on this, but the distinction is implicit in several design choices.

In first-order logic, a theorem like "the sum of two continuous functions is continuous" would need to be expressed with explicit quantification over the domain elements: ∀x.∀ε.∃δ... This works, but it forces the prover to discover and manipulate the ε-δ definitions from scratch each time. In higher-order logic, "continuous" can be a predicate on functions (continuity : (ℝ→ℝ) → ℝ → bool), and theorems can quantify over functions directly. This means that the library can contain high-level theorems like "the composition of continuous functions is continuous" that operate on the function level, dramatically compressing proof search.

But this expressivity comes at a cost: the search space explodes. When a tactic allows instantiating a higher-order variable with any function of the appropriate type, the prover must somehow select the right function from a combinatorially vast space. Human mathematicians do this through insight and experience—recognizing that a particular lemma "feels right" for the current goal. An ML prover must learn to do the same, which requires learning rich representations of both the goal and the available theorems, exactly the kind of task that deep neural networks are suited for.

The paper's decision to restrict tactics to those that take only previously-proven theorems as arguments (not arbitrary terms) is a practical concession to this complexity. It means the action space is discrete and circumscribed: at each proof step, the ML model must select a tactic and then select which existing theorems to feed it as arguments. This is still a hard problem—the corpus contains 29,462 theorems, creating a premise selection problem of considerable scale—but it is tractable in a way that full term generation would not be.

How the Paper Positions Itself

The paper positions HOList as the missing infrastructure that will enable ML researchers to attack higher-order theorem proving without first becoming experts in HOL Light or OCaml. The positioning is explicit in the contribution list (Section 1), which emphasizes packaging and accessibility:

"An instrumented, pre-packaged version of HOL Light that can be used as a reinforcement learning environment for theorem proving using our well-defined, stable Python API."

The word "stable" is doing significant work here. Prior ITP APIs were often fragile, deeply coupled to the OCaml runtime, and impossible to use in distributed settings. HOList provides a Docker container with all dependencies pre-built, a proof assistant API with two functions (apply tactic, register theorem), stateless tactic application for flexible proof search, and a proof checker that compiles discovered proofs back into OCaml for verification through HOL Light's trusted core.

Crucially, the paper does not claim to have solved theorem proving. DeepHOL is presented as a reference prover that "demonstrates the feasibility of the proposed learning task." The architecture is deliberately simple—breadth-first search guided by neural ranking of tactics and premises—to establish a baseline that future work can improve upon. The paper explicitly acknowledges that "the system can learn without any supervision or initial seed data" but that "preliminary experiments have shown that, in its current form, it learns inferior models compared to those that were seeded with human proofs." This is not presented as a failure but as a characterization of the learning difficulty: completely unsupervised exploration of the proof space is possible but inefficient, and the benchmark provides human proof logs precisely so that researchers can study the transition from imitation to self-improvement.

The paper also positions itself at a specific point in the scaling hierarchy. The Flyspeck corpus at ~30K theorems is large enough to require learning (a human cannot memorize it) but small enough that experiments are feasible (the RL loop runs on ~1000 cores, which is significant but within reach of academic or industrial compute budgets). This is in contrast to much larger libraries (Mizar's 50K+ theorems) or much smaller ones (GamePad's 1602). The paper implicitly argues that this intermediate scale is the sweet spot for current ML research: large enough to force generalization but small enough to enable rapid experimentation.

Finally, the paper positions its neural architecture as generic and transferable. Section 5 states:

"All the engineering went into the neural network architecture, which is very generic, and into maintaining the proof search graph without any special regard for the particular ITP system. In other words, DeepHOL currently uses HOL Light and its logic (HOL), but is not specialized to it. We believe that our solution would also work with other goal-tactic based prover like Coq, HOL4, or Lean."

This claim of generality is important because it addresses the fragmentation problem head-on. If DeepHOL's architecture is truly ITP-agnostic, then progress on the HOList benchmark should transfer to other proving systems, breaking the cycle of each ITP having its own bespoke ML approach. The two-tower architecture—one tower encoding the goal, one encoding the premises, with a combiner that scores their compatibility—is indeed a general framework that maps naturally to any tactic-based prover, though the paper does not empirically demonstrate this transferability.

3. Technical Approach

3.1 Reader Orientation

The system described in this section is DeepHOL, a fully learned automated theorem prover for higher-order logic that decides which proof step to take next by ranking possible actions—(tactic, arguments) pairs—using a neural network, then searches breadth-first through the resulting proof tree. It solves the problem of automating proof construction in an interactive theorem prover (ITP) without hand-crafted heuristics: given a goal statement (a formula to be proved), the system must repeatedly select which tactic to apply and which previously-proved theorems to feed it as arguments, doing this iteratively until all subgoals are closed. The "shape" of the solution is a two-tower neural architecture (one tower encoding the goal, one tower encoding every available premise theorem) whose outputs feed into two prediction heads—one for tactic classification and one for premise ranking—with the whole system trained first by imitation learning on human proof logs, then refined through a distributed reinforcement learning loop that mixes freshly self-generated proof traces with historical examples.

3.2 Big-Picture Architecture (Diagram in Words)

The DeepHOL prover has five major components:

1. Action Generator — the neural subsystem that, given a current goal (a formula to be proved), produces a priority-ordered list of (tactic, argument-list) pairs to try. It decomposes this into two subtasks: ranking all 41 available tactics, and for each tactic, ranking all theorems in the available library as potential arguments.

2. Two-Tower Neural Network — the learned model at the heart of the Action Generator. A Goal Encoder (G) maps the current goal expression (an S-expression string) to a fixed-length embedding vector. A Premise Encoder (P) does the same for each available theorem. A Combiner Network (C) takes the concatenation of the goal embedding and a premise embedding (and optionally a tactic embedding) and outputs a scalar score for how useful that premise is as a tactic argument for that goal.

3. Proof Search Graph — the data structure that tracks the state of the ongoing proof search. Nodes are goals (the original theorem and all subgoals generated by tactic applications). Hyperedges are tactic applications that transform a parent goal into one or more child subgoals. The graph supports subgoal sharing (identical subgoals discovered by different paths point to the same node) and automatic propagation of closed/failed statuses.

4. Proof Search Procedure — a simple breadth-first search that iteratively expands leaf nodes (unexplored subgoals) by calling the Action Generator, applies the ranked tactic applications in order, and stops when either a complete proof is found, a node limit is hit, or a timeout expires.

5. Reinforcement Learning Loop — a continuously running distributed system where trainer processes consume proof traces (from human logs and from the prover's own successful runs) to update the neural network, while multiple prover workers fetch the latest model checkpoint and attempt to prove randomly sampled training-set theorems, generating fresh training data that is mixed into the next training batches.

Information flows as follows: a theorem statement enters the system → the Proof Search procedure identifies it as an unexplored leaf node → the Action Generator encodes the goal through tower G, encodes all available premises through tower P, computes tactic scores via head S and premise scores via combiner C → the top-ranked (tactic, arguments) pairs are applied through the HOL Light API → resulting subgoals become new leaf nodes in the Proof Search Graph → sharing and status propagation prune redundant exploration → when a proof is found, it is serialized and its intermediate goals become training examples for the RL loop → the RL loop updates the neural network weights → subsequent proof attempts use the improved model.

3.3 Roadmap for the Deep Dive

• First, the HOL Light instrumentation layer and the Python API it exposes—this is the "physics engine" that DeepHOL interacts with, and understanding its stateless tactic application model and fingerprint-based theorem referencing is essential for understanding why the proof search graph can operate as it does.
• Second, the representation of mathematical expressions as normalized S-expressions—this defines the input format that the neural network sees and determines what information is and is not available to the learned model.
• Third, the Action Generator decomposition into tactic classification and premise ranking—this is the core architectural decision that structures the learning problem.
• Fourth, the two-tower neural architecture in detail, including the Goal Encoder, Premise Encoder, Tactic Classifier, and Combiner Network—this explains how embeddings are computed and combined to produce action scores.
• Fifth, the Proof Search Graph data structure and the breadth-first search algorithm—this explains how neural predictions are used to actually construct proofs, including critical features like subgoal sharing.
• Sixth, the supervised training procedure using human proof logs—this is the initialization phase.
• Seventh, the reinforcement learning loop architecture, including the four training example pools, proof pruning for high-quality training data, and the continuous mixing strategy—this is the self-improvement phase that pushes performance beyond imitation learning.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a systems and infrastructure paper whose core idea is that higher-order interactive theorem proving can be made accessible to deep reinforcement learning by (a) packaging an ITP as a stable, stateless Python API, (b) decomposing proof step prediction into a two-tower neural ranking problem, and (c) running a distributed RL loop that continuously mixes human and self-generated proof traces to bootstrap from imitation to autonomous theorem proving.

HOL Light Instrumentation and the Proof Assistant API

The foundation of the entire system is a modified version of the HOL Light interactive theorem prover that exposes a minimal, stable API through which external processes (written in Python, using TensorFlow) can drive proof search. Without this instrumentation, researchers would need to write proof search code directly in OCaml—HOL Light's implementation language—which would create an enormous barrier to using modern deep learning frameworks. The paper's solution is to turn HOL Light into a stateless "tactic execution engine" accessible over a simple protocol.

Why a fixed, pre-packaged version matters. Interactive theorem provers are living software systems: their tactic libraries evolve, new theorems are added, and the exact behavior of a tactic can change between versions. For a machine learning benchmark to be reproducible, the environment must be frozen. The paper addresses this explicitly:

"In order to create a stable, well-defined environment, we fix a particular version of HOL Light with a pre-selected subset of tactics and a fixed library of basic theorems, which are proved in one well-defined order."

This means that every researcher who downloads the HOList Docker container gets identical theorem statements, identical tactic behavior, and identical proof dependency ordering—no hidden variation that could confound comparison of results.

The two-function API. The Proof Assistant API exposes exactly two operations, both accessible from Python via the OCaml foreign-function interface:

Function 1: Stateless tactic application. The external prover sends a triple (goal, tactic_ID, argument_list) to HOL Light, where goal is a formula expressed as an S-expression string, tactic_ID specifies which of the 41 available tactics to apply, and argument_list is a list of previously-registered theorems (referenced by fingerprint number, not by their full text). HOL Light applies the tactic to the goal with those arguments and returns one of two outcomes: failure (the tactic's preconditions are not met) or success with a list of subgoals that must now be proved for the original goal to be considered proved. If the subgoal list is empty, the goal is fully proved and no further work is needed for that branch.

The statelessness of this interface is a deliberate design choice that the paper highlights:

"The stateless tactic application interface frees us from the strict order on subgoals that HOL Light enforces in the human interface, and allows us to easily implement more advanced proof search strategies."

In the human-facing HOL Light interface, subgoals must be proved in a specific order (typically depth-first, left-to-right), and the system maintains an internal stack of pending goals that the user cannot reorder. By making each tactic application a pure function of its inputs, the API enables the proof search graph to explore subgoals in any order—breadth-first, best-first, or with prioritization heuristics—without fighting against HOL Light's internal state machine.

Function 2: Theorem registration. Before a theorem can be referenced as a tactic argument, it must be registered with the HOL Light instance and assigned a fingerprint number. The registration function takes a theorem (its statement and its HOL Light internal proof object) and returns an integer fingerprint that can then be used in subsequent tactic application calls. The paper explains the motivation:

"Implemented naively, this [theorem] list could make the tactic application request very large and could slow down the prover. In the argument list of tactics we therefore allow theorems to be referenced by a fingerprint number."

This is a practical optimization that has architectural implications. Because theorems are referenced by fingerprint rather than by value, the Proof Search Graph can store compact references rather than duplicating full theorem texts at every node. And because registration is stateful (the mapping from fingerprints to theorems persists within a HOL Light session), subsequent tactic applications are fast network calls carrying only small integers rather than multi-kilobyte S-expression strings.

Fast startup via lazy theorem registration. The paper identifies a critical practical barrier:

"Starting HOL Light and loading all the potentially needed libraries can take a long time—we measured it at up to 20 minutes. This would be inhibitively long for proof search, especially in a distributed setting with thousands of workers and the startup time has to be paid for every worker."

The solution is to load only a minimal core of HOL Light (the trusted kernel and basic tactics) at startup, which takes "mere seconds," and then register all remaining theorems from the libraries on-demand through the API. This transforms the startup cost from a 20-minute sequential bottleneck to a few seconds of OCaml initialization plus the time to register theorems through the Python interface. In a distributed setup with 1000 worker processes, this reduction is the difference between a viable system and an infeasible one—a 20-minute startup per worker would consume over 300 CPU-hours just to initialize a single round of proof search.

The trusted core and proof checking. HOL Light is architecturally different from most software in a way that is crucial for theorem proving: it is built around a small "trusted core" of approximately 400 lines of OCaml code that implements the primitive inference rules of higher-order logic (modus ponens, universal generalization, lambda calculus conversion, etc.). Every theorem proved in HOL Light is ultimately a data structure whose type is thm, and OCaml's type system guarantees that objects of type thm can only be constructed by calling functions from the trusted core. Any bug in the rest of HOL Light—the tactics, the pretty-printer, the proof management system—cannot produce an invalid theorem, because those components can only manipulate thm objects through the trusted-core API.

The HOList environment, however, allows proof search to happen outside OCaml, in Python processes that have no access to the trusted core. This creates a trust problem: if a bug in the Python proof search code incorrectly claims to have found a proof, how can we be sure the proof is valid? The paper addresses this with a proof checker:

"The proof checker compiles proofs into OCaml code that can be loaded in HOL Light, where they have to pass through the trusted core."

The mechanism is: when DeepHOL's proof search finds a complete proof (a tree of tactic applications leading from the original goal to empty subgoal lists at every leaf), it serializes the entire proof tree. This serialized proof is then translated into an OCaml script that re-executes every tactic application in sequence within a fresh HOL Light instance. If the OCaml script runs without error through the trusted core, the resulting thm object is guaranteed to represent a valid proof. If any step fails (because the Python code made an incorrect claim, or because the serialization lost information), the proof is rejected. This means researchers can implement arbitrary search algorithms in Python without worrying about soundness—the proof checker is the final arbiter.

Fixed tactic set and argument restrictions. The environment restricts the available tactics to a "preselected small set of tactics (currently consisting of 41 tactics)" and further restricts tactic arguments to "a previously proven theorem or a list of previously proven theorems." Tactics that take arbitrary terms as arguments—for example, a tactic that requires the user to supply a witness term for an existential quantifier—are explicitly excluded:

"(There are also tactics that take terms as arguments, but we do not support them currently.)"

This restriction transforms the action space from the continuous (generating arbitrary well-typed HOL terms) to the discrete (selecting from a finite, though large, library of existing theorems). This is a significant simplification that makes the learning problem tractable for current neural architectures. The tradeoff is that some human proofs that rely on term-argument tactics cannot be replicated; the environment's benchmark is therefore a subset of what a human can do in HOL Light, but a subset that is large enough (29,462 theorems) to be practically meaningful.

Representation of Expressions as Normalized S-Expressions

All mathematical expressions in HOList—goal statements, theorem statements, hypotheses—are represented as S-expressions (symbolic expressions), a parenthesized prefix notation that unambiguously encodes the abstract syntax tree of a HOL term. The paper describes the format concisely:

"All expressions are presented as S-expressions that have only few types of non-leaf nodes: function applications, abstractions (i.e. lambda functions), variables, constants, and function types. All other information, such as variable names, constant names, and type names, is given as leaf-nodes."

For example, the expression f(x) where f is a function of type ℝ → ℝ would be represented as:

(a (v (fun (real) real) f) (v real x))

Breaking this down from the inside out: (fun (real) real) is the type of functions from real to real; (v (fun (real) real) f) declares a variable f of that type; (v real x) declares a variable x of type real; and the outermost (a ... ...) is a function application node that applies the first sub-expression (f) to the second (x). This prefix, fully-parenthesized format is isomorphic to a tree, which means it can be parsed deterministically into a tree structure, though the paper notes that "our current models only observe the string version of these expressions" rather than exploiting the tree structure explicitly.

Length and vocabulary characteristics. The S-expression representation is verbose:

"Expressions are quite long in this representation: The average number of tokens in the goals is around 500, and the median is around 300."

A 500-token string is well within the capacity of modern sequence models (transformers routinely handle thousands of tokens), but it is substantially longer than typical NLP inputs and means that the neural encoder must learn long-range dependencies across deeply nested parenthesized structures. This is one motivation for the choice of WaveNet—a dilated convolutional architecture—as the encoder, since WaveNet's exponentially growing receptive field is well-suited to capturing hierarchical structure in sequences.

The normalization problem. HOL Light, like many ITPs, automatically generates fresh names for generic type variables and term variables during proof construction. These machine-generated names are unique across the entire system—a typical proof of a calculus theorem might introduce temporary type variable ?345882 and term variable GEN%PVAR%9675 that appear nowhere else. The paper identifies two problems with leaving these names in the training data:

1. Embedding sparsity: "This leads to thousands of types and variables that often occur in only one (or a few) expressions, and hence would hardly get meaningful embeddings in typical deep learning approaches." If a token appears once in the entire corpus, its embedding vector will be essentially random and untrained, adding noise to the model's representations.

2. Information leakage: "Tokens that are shared only between few expressions bear the risk of unintentionally giving away information about the relations between these statements." If two otherwise-unrelated goals happen to share a machine-generated variable name, the model might learn a spurious correlation that does not generalize.

The solution is normalization:

"We therefore decided to normalize the data sets by mapping generic types and generic variables to a much smaller set of names while maintaining the semantics of all expressions."

The normalization procedure replaces each unique machine-generated name with a canonical name drawn from a small, fixed vocabulary, ensuring that structurally identical expressions (differing only in the arbitrary names assigned to their bound variables) map to identical normalized forms. After normalization, "the number of distinct tokens is 1254," a vocabulary size that is trivially manageable for neural embedding layers and small enough that every token will appear many times in the training corpus, allowing meaningful embedding learning.

This normalization is a form of alpha-renaming (the consistent renaming of bound variables) that is standard in formal logic but that must be implemented carefully to preserve semantics: the normalization must respect variable scoping so that two occurrences of ?345882 that are actually different variables (because one is bound in an inner lambda and the other is free) are not conflated. The paper does not detail the normalization algorithm, but the constraint that it "maintain[s] the semantics of all expressions" implies that it performs a scope-respecting canonicalization.

The Action Generator: Decomposing Proof Step Prediction

At each step of proof search, the system must decide: given the current goal (what we are trying to prove), which of the 41 available tactics should we apply, and which of the thousands of previously-proved theorems should we pass to it as arguments? The Action Generator is the component that answers this question. The paper describes its role:

"The most crucial part of our prover is the action generator that produces a list of tactic applications for a given goal. We have split this into two subtasks: To rank the tactics, and to create an argument list for each of the tactics (comprised of a list of theorems)."

This decomposition is both architectural (the neural network has separate prediction heads for tactics and arguments) and procedural (the system first scores all tactics, then for the highest-scoring tactics, scores all available premises as arguments).

Why two subtasks rather than a joint prediction? A joint prediction over all possible (tactic, argument_list) pairs would face a combinatorially enormous output space: with 41 tactics and 29,462 available theorems, there are 41 × (2^29462) possible argument combinations (since each theorem can be included or not in the list). This is obviously intractable. The decomposition into tactic_score(tactic | goal) and argument_score(theorem | goal, tactic) reduces the problem to two tractable ranking problems: a 41-way classification and an independent binary relevance score for each premise theorem. The independence assumption (that the relevance of theorem A does not depend on whether theorem B is also in the argument list) is a simplification, but it is the same simplification made by most information retrieval and recommendation systems, and it works well enough in practice.

Tactic ranking first, argument ranking second. The pipeline is: for a given goal, compute the goal embedding (a single forward pass through the Goal Encoder tower). Feed this embedding through the Tactic Classifier head S to obtain 41 logits. The top k tactics by score are then considered for argument ranking. For each of these top k tactics, the system ranks all available premises using the Combiner Network C, which takes [goal_embedding, premise_embedding, (optionally) tactic_embedding] and outputs a scalar score. The final output is an ordered list of (tactic, [theorem_1, theorem_2, ...]) pairs, where each argument list is constructed by taking the top-scoring premises for that tactic, up to a fixed length limit.

Scope of available premises. The set of premises available as arguments is not the entire 29,462 theorems—it is limited to "all possible tactic arguments t_i in the scope of the goal to be proved." In HOL Light, this means theorems that have already been proved and registered before the current goal in the dependency-ordered library. The paper provides "all theorems in the three corpora in one unified list, in the order they were proven by humans," which determines exactly which theorems are in scope for any given goal. This is a realistic constraint that mirrors the human proving experience: you cannot use a theorem that hasn't been proved yet.

Two-Tower Neural Architecture

The neural network that powers the Action Generator follows a two-tower architecture, a design pattern common in information retrieval and recommendation systems where queries and documents are encoded separately and then compared via a lightweight combiner. Figure 1 in the paper provides the schematic, and the prose describes it as:

"The neural network has two separate prediction heads S and R. The goal tower G computes an embedding G(g) of the current goal g and infers a scoring vector S(G(g)) for the fixed set of tactics where the tactic classifier S is a linear layer producing logits of a softmax classifier. The premise tower P computes a fixed size embedding P(t_i) of all possible tactic arguments t_i in the scope of the goal to be proved."

Let us trace through each component precisely.

#### Goal Encoder (Tower G)

The Goal Encoder takes as input a single goal, which is a HOL Light term represented as a normalized S-expression string. The paper notes an important preprocessing step:

"(In HOL Light, each goal consists of a list of hypotheses and a conclusion, and we currently drop the hypotheses before we feed a goal to the neural network.)"

This means the encoder sees only the conclusion (the statement to be proved), not the assumptions under which it must be proved. For many tactics, the hypotheses are essential for deciding which tactic to apply—for example, a hypothesis of the form A ∧ B can be broken into A and B using a conjunction-elimination tactic—so dropping them is a significant information loss. The paper does not justify this design choice explicitly, but it is likely a pragmatic simplification: including hypotheses would make the input even longer (the average goal already has 500 tokens), and the hypotheses are typically derivable from the conclusion via well-typed inference rules, so a sufficiently powerful encoder might learn to infer the relevant hypothesis structure from the conclusion alone.

The encoder architecture is based on WaveNet (Van Den Oord et al., 2016), originally developed for raw audio generation. WaveNet uses dilated causal convolutions, where the dilation factor doubles at each layer, creating an exponentially growing receptive field without increasing the number of parameters. This is particularly appropriate for S-expressions because: (a) S-expressions have deeply nested structure where matching parentheses can be hundreds of tokens apart, requiring long-range dependencies; (b) the hierarchical structure of mathematical terms matches the exponentially growing temporal scope of dilated convolutions; and (c) WaveNet is computationally efficient for long sequences compared to quadratic-attention transformers.

The paper reports experiments with different WaveNet configurations:

• Base WaveNet: "two WaveNet blocks of four layers each. The number of filters in each block was either 128 or 256." This is a relatively shallow, narrow configuration with 2 × 4 = 8 total convolutional layers.
• Deeper WaveNet: "four blocks of five layers each, in this case with depth 128." This is 4 × 5 = 20 total convolutional layers, a substantially deeper network. The paper reports that this "deeper network with more blocks, which has 47 million parameters, turned out to be superior."

The output of the Goal Encoder is a fixed-length embedding vector G(g) ∈ ℝ^d (where d is the filter depth, either 128 or 256 depending on the configuration) that represents the entire goal expression in a continuous vector space optimized for the downstream prediction tasks.

#### Premise Encoder (Tower P)

The Premise Encoder has an identical architecture to the Goal Encoder (WaveNet with the same number of blocks and filters) but separate weights. This weight separation is important: goals and premises are syntactically similar (they are both HOL formulas), but they play semantically different roles in the prediction task. A goal is "what we want to prove," while a premise is "something already known that might help." Sharing weights would force the same representation to serve both roles, potentially losing information. Separate towers allow G to learn goal-specific features (e.g., "this goal has an existential quantifier that needs to be instantiated") while P learns premise-specific features (e.g., "this theorem provides a witness for existential goals of a certain shape").

The Premise Encoder maps each theorem t_i in the available library to a fixed-length embedding P(t_i) ∈ ℝ^d. For a library of M theorems, this produces an M × d matrix of premise embeddings.

Precomputation for efficiency. The paper describes a critical optimization:

"At the start of each round, we fetch the latest trained model checkpoint and precompute the theorem argument embedding for each theorem in the complex and core libraries. This precomputation greatly accelerates the ranking of the tactic arguments."

Because the available premises do not change during a proof search round (the library is fixed), all premise embeddings can be computed once at the start of the round, cached, and reused for every goal encountered during proof search. This reduces the per-goal cost from "encode goal + encode M premises" to "encode goal + M dot products with cached premise embeddings," which is a massive speedup when M ≈ 30,000. Without this precomputation, the Action Generator would be impractically slow for interactive proof search.

#### Tactic Classifier (Head S)

The Tactic Classifier is a linear layer that takes the goal embedding G(g) as input and outputs a vector of 41 logits (one per available tactic):

$s_{\text{tactic}}(j \mid g) = \mathbf{W}_S \cdot G(g) + \mathbf{b}_S$

where $\mathbf{W}_S$ is a $41 \times d$ weight matrix, $\mathbf{b}_S$ is a 41-dimensional bias vector, and $s_{\text{tactic}}(j \mid g)$ is the unnormalized score for tactic $j$ given goal $g$.

What it computes: for a given goal embedding, the Tactic Classifier produces 41 real-valued scores, which are converted to a probability distribution over tactics via softmax. The system uses these scores to rank tactics: higher-scoring tactics are tried first during proof search.

Why a linear classifier rather than a deeper network: the goal embedding G(g) has already undergone deep nonlinear processing through the WaveNet tower. A linear classifier on top of this embedding is sufficient to learn decision boundaries between tactic classes, and adding more layers would increase parameters without necessarily improving the quality of the learned embedding (since the linear classifier's gradient signal backpropagates through the entire WaveNet, shaping the representation). This is the standard design pattern in representation learning: a deep encoder produces a rich embedding, and shallow task-specific heads consume it.

The paper reports that tactic prediction accuracy "rang[es] between 38% and 42% for most models" on the validation set. This is substantially above the random baseline of 1/41 ≈ 2.4%, indicating that the model has learned non-trivial associations between goal structure and appropriate tactics, but it is far from perfect, reflecting the inherent ambiguity of proof step selection (multiple different tactics can legitimately be applied to the same goal, and the "correct" one in the human proof log is only one of potentially many valid choices).

#### Combiner Network (Head C) and Theorem Scorer

The Combiner Network is where the two towers meet. It takes the concatenation of three embeddings—the goal embedding G(g), a premise embedding P(t_i), and optionally a tactic embedding T_j—and outputs a single scalar score:

$r(t_i) = C(G(g), P(t_i), T_j)$

where $r(t_i)$ is "the score of theorem $t_i$ for its being a useful tactic argument for transforming the current goal $g$ towards a closed proof."

The paper describes two variants of the combiner:

1. Tactic-conditioned: $r(t_i) = C(G(g), P(t_i), T_j)$. The score for a premise depends on which tactic is being applied. This makes intuitive sense: a theorem that is useful as an argument to REWRITE_TAC (which rewrites the goal using an equation) might be useless as an argument to MESON_TAC (which calls a first-order prover). Different tactics consume theorems of different logical forms.

2. Tactic-independent: $r(t_i) = C(G(g), P(t_i))$. The score for a premise is independent of which tactic will be applied. This is simpler and might work if the premise encoder learns to embed theorems in a way that captures their general relevance to the goal, regardless of the specific tactic.

The paper's reinforcement learning experiments compare these two variants (Table 2): the "Loop" experiment uses tactic-independent argument selection, while the "Loop tactic dependent" experiment conditions on the tactic. The tactic-dependent variant achieves higher final performance (38.9% vs. 36.3%), confirming that premise relevance is indeed tactic-specific.

The Combiner Network is implemented as "fully connected combiner layers with additional dropout layers before each of them," with a dropout rate of 0.3 during training. The exact architecture (number of layers, hidden dimensions) is not specified beyond the statement that they are "fully connected," but the typical pattern in two-tower architectures is 2–3 fully connected layers that progressively reduce the concatenated embedding dimension to a scalar.

Why a separate combiner rather than a dot product: in many two-tower architectures (especially for retrieval), the final score is simply the dot product G(g) · P(t_i), which enforces that relevance is bilinear in the two embeddings. The DeepHOL combiner, by using fully connected layers, can learn nonlinear interactions between the goal and premise representations—for example, it can learn that a premise about ∀x. P(x) → Q(x) is highly relevant to a goal of the form Q(a) but only when there is also a hypothesis P(a) in context (which the goal encoder might have captured even if the hypotheses are dropped from the input string). This nonlinearity is important for mathematical reasoning, where relevance often depends on matching specific subterms or logical forms.

Proof Search Graph

The Proof Search Graph is the runtime data structure that manages the state of an ongoing proof attempt. It is not a learned component but a carefully designed bookkeeping system that enables efficient, redundancy-free exploration. The paper describes it as:

"The nodes of the proof search graph are the goals that we have seen in the proof search, including the original goal statement that we want to prove. Each goal can have multiple alternative tactic applications, each of which might result in multiple subgoals. That is, tactic applications are labelled hyperedges in the proof search graph."

Nodes as goals, hyperedges as tactic applications. A "normal" graph edge connects two nodes. A hyperedge connects one parent node to multiple child nodes simultaneously. This maps exactly to the structure of proof search: applying a tactic to a goal produces zero or more subgoals. If a tactic produces zero subgoals, the hyperedge has no children and the parent goal is considered proved. If it produces k > 0 subgoals, the hyperedge has k children, all of which must be proved for the parent to be proved (an AND relationship). If there are multiple hyperedges from the same goal (alternative tactic applications), any one of them succeeding is sufficient to prove the goal (an OR relationship).

Three pruning mechanisms prevent the search graph from exploding:

1. Closed-goal propagation. When a tactic application produces an empty subgoal list—meaning that branch is fully proved—this success is propagated upward through the proof graph:

"Whenever a tactic application closes a subgoal, this information is traced back to the parent subgoals and each alternate tactic application (and its whole sub-branch) is marked as closed and discarded from the queue to be processed."

The idea is: if goal G has three alternative hyperedges A, B, and C, and hyperedge A succeeds (all its subgoals are eventually proved), then B and C become irrelevant and their entire subtrees can be pruned, freeing compute resources. If this propagation reaches the root node (the original theorem), the entire proof is complete and the search terminates.

2. Failed-goal propagation (AND-compression). The inverse of closed-goal propagation: if all hyperedges from a goal fail, the goal itself is marked as failed, and this failure propagates to its siblings:

"When all tactic applications for a goal fail we mark that goal as unsuccessful. Similar to tracing closed goals, the proof search graph automatically traces the siblings of unsuccessful subgoals that become superfluous, and mark them unsuccessful as well."

Since subgoals from the same tactic application are AND-related (all must succeed), failure of any one subgoal means the entire tactic application fails, and the remaining sibling subgoals become irrelevant and can be pruned. This is a standard AND-OR graph search optimization.

3. Subgoal sharing. This is the most distinctive feature of the Proof Search Graph and the one that the paper argues is "crucial":

"When tactic applications produce identical subgoals, we let them point to the same node in the proof search graph."

In mathematical proofs, the same intermediate lemma often arises from different reasoning paths. For example, proving A ∧ B and proving B ∧ A both require proving A and B as subgoals, just in different orders. Without subgoal sharing, the search would prove A twice, wasting computation. With sharing, once A is proved (or failed), all parent goals that depend on A are immediately updated. The paper provides a concrete example of why this matters:

"Without subgoal sharing the search process could end up oscillating between two formulas by rewriting the same subterm back and forth using the same equation."

This is a well-known problem in rewriting-based proof search: applying equation E: a = b to rewrite a to b, then later applying E again (or its symmetric version) to rewrite b back to a, creating an infinite loop. Subgoal sharing detects that the intermediate goal b = target has been seen before, preventing redundant (and potentially infinite) re-exploration.

The implementation detail: "once a subgoal is newly shared, previously stored information about subgoals being closed or ignored is propagated through the search graph." This means that if goal X is proved, and later a new hyperedge is discovered that also produces X as a subgoal, the new hyperedge immediately benefits from X's already-proved status without re-proving it.

Proof Search Algorithm

The proof search is "a simple breadth first search." The paper describes the per-iteration procedure:

"In each iteration, it expands all leaf nodes (i.e. goals that have not been expanded yet). To expand a goal, it calls the action generator to generate a list of tactic applications, and applies them in order."

The expansion of a single goal follows this subroutine:

1. Call the Action Generator with the goal, obtaining a ranked list of (tactic, argument_list) pairs.
2. Apply each tactic application in rank order (highest score first) through the HOL Light API.
3. Stop when one of two stopping conditions is met: "when it reaches a maximum number of unsuccessful tactic applications or a minimum number of successful tactic applications."
4. Successful tactic applications add their subgoals as new leaf nodes in the Proof Search Graph.
5. Unsuccessful tactic applications are counted toward the "maximum unsuccessful" limit; once that limit is reached, further lower-ranked tactics are not even tried, saving computation.

The purpose of these stopping conditions is to prevent a single goal from consuming all available budget. If the top-ranked tactics all fail, continuing to try the 30th-ranked tactic is almost certainly a waste of time. Conversely, if several high-ranked tactics succeed (producing subgoals that might be provable), exploring even more tactics is unnecessary—the prover already has viable paths to explore.

Global stopping conditions. The entire proof search terminates under any of three conditions:

1. Success: "Whenever a complete proof is found for the top level goal, the proof search is stopped and the whole proof search graph is serialized and stored as the result."
2. Node limit: "The proof search finishes if the search graph reaches a prescribed limit on the number of subgoals." This prevents unbounded memory consumption on hard theorems.
3. Timeout: "The proof search times out." The paper specifies "a computation limit of 100 explored proof states and a total timeout of 300 seconds" for the RL loop experiments.

Randomization of search parameters. During reinforcement learning, the prover deliberately varies its search parameters to increase proof diversity:

These are sampled uniformly from the specified ranges for each proof attempt. The goal is to prevent the RL loop from converging to a narrow set of proof strategies: by sometimes exploring more tactics (up to 16 top-ranked), sometimes accepting more successful applications (up to 6), and sometimes using longer argument lists (up to 32 theorems), the prover generates a more diverse set of training traces, which helps the model generalize rather than overfit to a single search configuration. The paper states this explicitly:

"Additionally, for each example, we pick prover options uniformly in the ranges described by Table 3, to increase the diversity of the generated proofs. This also increases the chance of finding a proof at all for harder statements."

Supervised Learning from Human Proof Logs

The initial training of DeepHOL uses imitation learning: the model learns to predict which tactic and arguments a human used at each step. The data source is the proof logs generated by HOL Light's instrumented prove method:

"We have instrumented the prove method in HOL Light with extra logging code. If HOL Light is executed in proof-dump mode, each invocation of the prove function dumps the proven theorems and their proofs into files."

Each training example extracted from these logs consists of four components:

1. goal: a provable statement—either a top-level theorem from one of the three corpora, or a subgoal encountered during the proof of a top-level theorem.
2. tactic: the integer ID of the tactic (out of 41) that the human applied to this goal.
3. arglist: the list of theorems (referenced by their positions in the dependency-ordered library) that the human passed as arguments to the tactic.
4. negarglist: a list of "hard negative" theorems—theorems that scored highly under the model but were not actually needed. This list is empty for examples generated from human proof logs (since humans don't generate false positives) and is populated only during reinforcement learning.

Training objective. The model is trained with two losses:

• Tactic classification loss: cross-entropy between the predicted tactic distribution (41-way softmax) and the ground-truth human tactic.
• Premise ranking loss: a pairwise ranking loss that encourages the score of true premises (arglist members) to be higher than the score of hard negatives (negarglist members). The paper does not specify the exact loss function (e.g., whether it uses margin ranking loss, binary cross-entropy per premise, or something else), but the standard approach for such settings is to treat each premise independently as a binary classification problem (useful vs. not useful) or to use a pairwise hinge loss.

Training hyperparameters:

"All models were trained with the Adam optimizer and exponentially decreasing learning rate starting at 0.0001 with decay rate 0.98 at every 100000 steps. For evaluation, we use moving exponential parameter averaging at a rate of 0.9999 per step."

The moving average of parameters (Polyak averaging, references [48, 49]) is a standard technique for stabilizing model predictions: rather than using the raw parameters from the most recent training step (which may be noisy due to stochastic gradient variance), evaluation uses an exponentially weighted average of all past parameter values, with recent values weighted more heavily (decay 0.9999 per step means the half-life is roughly 6931 steps).

Data splits. The training examples are derived from theorems split 60:20:20 into training, validation, and test sets:

"Before training and evaluation, we have split the top level theorems into three subsets: training, validation and test set in a 60:20:20 ratio. Since the goals occurring in the proof of a theorem are likely correlated with the theorem itself, we assign them the same split as the theorem."

This last point is crucial for valid evaluation: if subgoals from a test-set theorem leaked into the training set, the model could memorize specific intermediate proof states and achieve inflated test performance. By assigning the entire proof tree (theorem + all subgoals) to the same split, the paper ensures that no information crosses the train/test boundary.

Reinforcement Learning Loop

The reinforcement learning loop is where DeepHOL moves beyond imitating humans and begins to discover proof strategies that humans did not use. The architecture is a continuously running distributed system:

"In the reinforcement learning loop, we have both a trainer and multiple provers running continuously."

The loop iteration. Each round of the loop proceeds as follows:

1. Fetch the latest trained model checkpoint.
2. Precompute premise embeddings for all theorems in the library (using the current Premise Encoder weights).
3. Randomly sample 2000 theorems from the training set (the union of core and complex corpora).
4. Distribute proof attempts for these 2000 theorems across 1000 CPU workers.
5. Each worker runs the Proof Search (Section 3.4.5) using the current model to guide action selection.
6. Successful proofs are serialized, and their intermediate proof states are converted into training examples.
7. These new training examples are added to the training pool.
8. The trainer samples batches from the training pool (mixing examples from different sources according to a prescribed ratio), updates the model, and produces a new checkpoint.
9. The next round begins from step 1 with the new checkpoint.

The four training example pools. The paper organizes training data into four distinct pools, mixed at batch construction time:

1. Human training examples as seed (optional): proof states extracted from human proof logs. These provide high-quality initial supervision.
2. Inherited computer-generated examples as seed (optional): examples generated during previous experiments. The paper notes: "we used examples that were generated by a prover that was run on the whole training set utilizing a model that was trained in purely supervised manner." This bootstraps the RL loop from a higher starting point.
3. Fresh generated loop examples: examples produced in the last k rounds, where k is a configurable parameter. These are the most on-policy examples because they come from the most recent model.
4. Historical training loop examples: examples produced in all rounds prior to the last k. These provide stability and prevent catastrophic forgetting of older proof patterns.

Mixing ratio. The paper specifies that "batches are filled with examples from each pool according to a prescribed split ratio." The exact ratio is not stated, but the key property is that "the ratio of different kinds of examples the model is trained on does not shift as more examples are generated by the loop." This is important because without fixed ratios, as the loop generates more and more self-generated examples, the training distribution would drift increasingly far from the human examples, potentially causing the model to forget human proof patterns entirely. The fixed ratio ensures that the human examples continue to exert influence even as the total number of examples grows.

Why fresh vs. historical matters. Fresh examples (from the last k rounds) are generated by a model that is closer to the current model, making them more on-policy. Historical examples are more diverse but potentially less relevant to the current model's behavior. By mixing both, the training procedure balances exploration (learning from diverse historical proofs) with exploitation (refining the proof strategies that the current model is actually discovering).

Preliminary note on unseeded learning. The paper explicitly acknowledges a limitation:

"Although we can make use of human and inherited proof traces, the system can learn without any supervision or initial seed data. However, preliminary experiments have shown that, in its current form, it learns inferior models compared to those that were seeded with human proofs."

This means that pure RL from scratch—exploring the proof space randomly and learning from whatever proofs are accidentally discovered—is theoretically possible but practically inefficient. The human proofs provide a curriculum that guides the model toward productive regions of the search space, without which the model spends too much time in dead ends. This is consistent with the broader RL literature, where pure exploration in combinatorially large action spaces almost always fails without some form of shaping or demonstration.

Proof Pruning for High-Quality Training Data

A critical quality issue arises in the RL loop: the argument lists generated by the model are deliberately long (to increase the chance of including a needed theorem), and they contain many theorems that are irrelevant to the proof's success. Training on these inflated argument lists would teach the model that irrelevant theorems are useful, degrading the premise ranking quality over time. The paper addresses this with a proof pruning procedure:

"For all tactics that take a list of theorems as an argument, our current implementation generates a list of fixed length. For successful tactic applications, we then iterate over the arguments in reverse score order and greedily omit those arguments that do not change the outcome of the tactic application."

The pruning algorithm works as follows:

1. A successful tactic application was made with argument list [t_1, t_2, ..., t_n], where the theorems are ordered by their Combiner Network score (highest to lowest).
2. Starting from the lowest-scoring theorem t_n, try removing it from the argument list and re-running the tactic application on the same goal.
3. If the tactic application still succeeds (produces the same subgoals, or at least still succeeds at all), then t_n was indeed superfluous—it is permanently removed from the argument list.
4. Continue upward through the list (t_{n-1}, t_{n-2}, ...), at each step trying the reduced argument list and keeping the removal if the result is unchanged.
5. When removal of a theorem changes the outcome (the tactic fails or produces different subgoals), that theorem is necessary and is kept. Stop the pruning there (since theorems above it in the sorted list are higher-scoring and even more likely to be necessary).

The paper explains the greedy (rather than optimal) nature:

"While a non-greedy approach might yield even shorter argument lists, it would also take longer to compute."

Finding the minimal subset of arguments that preserves the tactic's outcome is a set-cover-like problem and would require 2^n trials in the worst case. The greedy reverse-order approach requires at most n trials and, because the arguments are sorted by score, tends to remove the least-likely-to-be-useful theorems first.

Hard negative construction. The removed theorems are not discarded—they are stored as "hard negatives" in the negarglist field of the training example:

"Removed parameters are stored as 'hard negatives' and utilized during training."

This is a form of hard negative mining: the removed theorems were ranked highly by the model (otherwise they wouldn't have been in the argument list in the first place), yet they were not actually needed. Training the model to assign lower scores to these specific theorems directly addresses the model's most salient ranking errors. This is more effective than using random negative examples, which would be trivially easy for the model to distinguish from true positives and would contribute little learning signal.

Summary of Desugn Choices and Their Justifications

• Stateless tactic application API over stateful session: enables arbitrary proof search order (not just depth-first left-to-right) and simplifies distributed deployment.
• Fingerprint-based theorem referencing over full-text arguments: reduces network communication cost by orders of magnitude for tactic applications.
• Separate Goal and Premise towers with independent weights over shared weights: allows each tower to learn role-specific features—goals need to encode "what do I need," premises need to encode "what do I provide."
• WaveNet dilated convolutions over RNNs or transformers: exponentially growing receptive field matches the hierarchical structure of S-expressions; computationally efficient for sequences of 500+ tokens.
• Tactic-first, argument-second ranking over joint prediction: avoids combinatorial explosion of the joint (tactic × argument-combination) action space.
• Tactic-conditioned premise scoring over tactic-independent: acknowledges that different tactics consume theorems of different logical forms.
• Subgoal sharing in the proof search graph over independent tree search: prevents infinite rewriting loops and avoids redundant proof of identical subgoals.
• Breadth-first search over depth-first or best-first: simplicity; BFS is complete (will find a proof if one exists within the depth bound) and naturally compatible with the proof graph data structure.
• Fixed-ratio mixing of training pools over simply adding new examples to a growing dataset: prevents training distribution drift as the loop generates more self-generated proofs.
• Greedy reverse-order proof pruning over optimal minimal-subset selection: provides practical runtime (linear in argument list length) while achieving nearly minimal argument lists in practice.
• Polyak parameter averaging at evaluation over raw parameters: reduces variance from stochastic gradient noise, improving prediction stability during proof search.

4. Key Insights and Innovations

Innovation 1: Theorem Proving as a Tactic + Premise Decomposition — Not a Single End-to-End Prediction

The dominant framing in prior neural theorem proving work was to treat proof step prediction as a monolithic problem: given a proof state, predict the next action. Whalen's Holophrasm [21] attempted exactly this—training a single neural network to output the next proof step directly. The problem with this framing is that the action space in higher-order logic is combinatorially explosive: with 41 tactics and thousands of available premises, the space of possible (tactic, argument_combination) pairs is astronomical. Holophrasm's results—"mostly proofs for very simple theorems, especially in propositional logic"—are a direct consequence of this framing: the model can only learn when the action space is small enough for a monolithic predictor to cover.

DeepHOL's key conceptual move is to decompose the prediction into two tractable sub-problems that mirror how human mathematicians actually think about proof construction. First, decide what kind of move to make (which of the 41 tactics fits the shape of the current goal)—this is a 41-way classification problem, trivially tractable. Second, given the chosen tactic, decide which already-known facts to feed it—this is a ranking problem over a finite, though large, library. The decomposition is imposed architecturally: the Goal Encoder feeds a linear Tactic Classifier (S) for tactic selection, while a separate Combiner Network (C) scores premise relevance conditional on (or independent of) the chosen tactic.

Why this is a reframing rather than an engineering convenience. Prior work on premise selection—particularly Alemi et al. [19] and the non-deep ML tradition [32, 33, 35]—treated premise ranking as a standalone task disconnected from tactic choice. You rank premises by relevance to the goal, then hand them to an ATP and hope for the best. DeepHOL's framework connects these decisions: premise relevance is conditional on the tactic that will consume it. The same theorem might be scored highly when the planned tactic is REWRITE_TAC (which uses equations to rewrite the goal) and low when the planned tactic is MESON_TAC (which performs first-order reasoning). The Tactic-Dependent loop achieving 38.9% vs. the Tactic-Independent loop's 36.3% (Table 2) is direct evidence that this conditioning matters—the model learns tactic-specific premise utility.

This decomposition also reframes the learning problem from "predict what a human did" (standard imitation learning) to "predict actions that lead to closed proofs" (RL-compatible). The Tactic Classifier and Premise Scorer produce scores that can be used to rank and filter actions during search, not just to replicate the single action a human happened to choose. When the proof search explores 6–16 top tactics and 1–32 top premises (Table 3), it is exploiting exactly this decomposition: the model provides a distribution over promising actions, and search explores it.

The distinction from TacticToe [9] is instructive. TacticToe also operates at the tactic level, but it uses k-nearest neighbors on hand-engineered features to retrieve similar past proof states and their human-chosen actions. There is no decomposition into tactic type vs. arguments—the retrieval is a single similarity lookup. DeepHOL's learned decomposition is more flexible because it can recognize that two goals are similar in structure (meriting the same tactic) while requiring different specific premises, or vice versa.

Innovation 2: The Continuous RL Loop as a Mechanism for Escaping Imitation Learning's Ceiling Through Self-Generated Proof Diversity

The paper's central empirical finding is that reinforcement learning from self-generated proofs substantially outperforms pure imitation learning on human traces: the Loop Tactic Dependent model reaches 38.9% on the complex validation set vs. 31.72% for the best supervised WaveNet (Table 2). This is not an incremental gain—it represents a roughly 23% relative improvement in proof closure rate. But the conceptual contribution is not the raw number; it is the demonstration that a specific architecture of continuous mixing—rather than sequential fine-tuning—is what makes RL from self-generated proofs work for theorem proving.

The problem with naive RL in theorem proving. If you simply take a model trained by imitation, generate proofs with it, and fine-tune on those proofs, you face two failure modes. First, the generated proofs are a narrow subset of the proof space—the model tends to reproduce its existing strategies, so fine-tuning on its own output reinforces those strategies without discovering new ones. This is the "exploration problem" in combinatorial search spaces. Second, as the model changes, its generated proofs reflect progressively more off-policy behavior relative to the original human data, and the model can forget the human proof patterns that initially made it competent—catastrophic forgetting.

DeepHOL's solution has two architectural features that address these failures. First, the four-pool training mixture (human seed, inherited computer-generated seed, fresh loop examples, historical loop examples) with fixed mixing ratios. The fixed ratio ensures that even as the loop generates thousands of new examples, the human proofs retain their proportional influence. This prevents the distributional drift that would otherwise cause the model to converge to a narrow self-reinforcing strategy. The paper's explicit note that "the ratio of different kinds of examples the model is trained on does not shift as more examples are generated by the loop" is the linchpin—without it, RL would become progressively more self-referential and likely degrade.

Second, randomized search parameters (Table 3) force proof diversity. By varying the number of top tactics explored, the number of successful applications accepted, and the argument list length, the prover generates proofs with different structures from the same model checkpoint. A theorem that might be proved with a short 2-tactic proof under one configuration might be proved with a longer 8-tactic proof under another, exposing the model to a wider variety of intermediate proof states during training. This is not merely "we randomized things and it helped"—it is a deliberate mechanism for converting a single model's capabilities into a diverse training distribution, which is exactly what makes the RL loop self-improving rather than self-reinforcing.

Contrast with prior RL for theorem proving. Kaliszyk et al. [25] demonstrated RL with XGBoost and LIBLINEAR on hand-engineered features in a first-order setting, but their approach used a single training pool that grew without bound, and they did not have the fixed-ratio mixing that prevents distribution drift. Whalen [21] used pure RL from scratch with no human seed at all. DeepHOL's architecture—seeded RL with continuous fixed-ratio mixing and diversity-inducing randomization—represents a distinct point in the design space that prior work had not explored.

The finding that unseeded RL produces inferior models ("preliminary experiments have shown that, in its current form, it learns inferior models compared to those that were seeded with human proofs") is itself a valuable negative result. It establishes that for theorem proving at this scale, pure exploration is not viable—some form of demonstration is necessary to guide the model toward productive regions of the proof space. This is consistent with the broader RL literature but had not been empirically demonstrated for higher-order theorem proving at the scale of 30K theorems.

Innovation 3: The Proof Checker as a Trusted-Core Bridge Between Unverified Search and Formal Correctness

Most machine learning systems produce outputs that are judged by accuracy metrics—a 90% accurate image classifier is a good image classifier. Theorem proving is different: a prover that is correct 99% of the time and incorrect 1% of the time is worse than useless for formal mathematics, because a single false theorem can invalidate an entire formalization effort. This creates a unique verification requirement that has no analog in standard ML benchmarks.

The standard solution in ITP systems like HOL Light is the trusted core: a small (~400 lines) kernel of OCaml code that implements the primitive inference rules of higher-order logic, with the type system guaranteeing that any object of type thm was constructed by these rules. Any theorem proved within the OCaml process is therefore guaranteed correct. But DeepHOL's proof search runs outside OCaml, in Python processes using TensorFlow, which have no access to the trusted core. The Python code could—due to a bug, a serialization error, or a neural network hallucination—claim to have found a proof that is actually invalid.

The paper's solution is a proof checker that compiles discovered proofs into OCaml scripts and replays them through the trusted core. This is conceptually distinctive because it decouples proof search from proof verification, allowing the search component to be arbitrarily complex, buggy, or heuristic, while the verification component remains formally verifiable by virtue of being a thin wrapper around the trusted core. The paper frames this explicitly:

"The proof checker compiles proofs into OCaml code that can be loaded in HOL Light, where they have to pass through the trusted core."

Why this is not just an engineering detail. In most ML-for-theorem-proving work, the soundness of the prover depends on the correctness of the entire software stack—the ML model, the search algorithm, the API, the communication protocol. GamePad [10] inherits Coq's trusted core but still requires trusting the Python-Coq interface. TacticToe [9] runs within the HOL4 process and therefore doesn't face this trust gap, but at the cost of being deeply embedded in the OCaml runtime and inaccessible to Python-based ML frameworks.

DeepHOL's architecture makes a different tradeoff: accept that the Python-based search system is untrusted, and add a separate verification step that is formally sound. This is the same architectural principle that underlies proof-carrying code and witness extraction in formal methods: generate a candidate solution with an untrusted (potentially heuristic) procedure, then verify it with a trusted checker. The innovation here is applying this principle to neural theorem proving, where the "untrusted procedure" is a deep neural network guiding proof search, and the "trusted checker" is HOL Light's kernel.

The practical significance is that researchers can experiment with arbitrary neural architectures and search algorithms without worrying about soundness. If a new model architecture produces a proof that is logically invalid, the proof checker will reject it, and the benchmark metrics (which only count verified proofs) will reflect the true performance. This makes the HOList environment safe for aggressive experimentation in a way that prior environments, where correctness depended on the entire pipeline, were not.

Innovation 4: The Three-Corpus Benchmark Structure as a Diagnostic Taxonomy of Mathematical Difficulty

Most ML benchmarks provide a single test set with a single accuracy number. HOList provides three distinct corpora—core (2,320 theorems), complex (16,623 theorems), and flyspeck (10,519 theorems)—that represent fundamentally different kinds of mathematical reasoning. The paper does not present this as merely "we have a lot of data"; it presents it as a stratified benchmark where performance across corpora diagnoses different capabilities.

• Core contains the foundational theorems of higher-order logic: properties of equality, basic type operations, the definitions that make the tactics work. These are the "axioms and basic lemmas" that everything else builds on. Performance on core indicates whether a prover has mastered the basic inference rules.
• Complex contains theorems of complex analysis: properties of analytic functions, contour integrals, Cauchy's theorem, and related results. These require domain-specific reasoning about limits, convergence, and complex-valued functions. Performance on complex indicates whether a prover can handle mathematical content beyond pure logic.
• Flyspeck contains the lemmas of the Kepler conjecture formalization: results in measure theory, polyhedral geometry, linear algebra, and multivariate analysis. These are the most diverse and application-oriented theorems. Performance on flyspeck indicates whether a prover can handle the kind of heterogeneous mathematical content that appears in real formalization efforts.

Why this is structurally different from prior benchmarks. HOLStep [24] provided a single static dataset without distinguishing between mathematical domains. GamePad [10] provided 1,602 theorems covering the Feit-Thompson theorem formalization, but this is essentially a single mathematical development in group theory—it does not span multiple domains. The HOList benchmark, by deriving from the Flyspeck formalization which "required formalizing a significant part of arithmetic, linear algebra, and multivariate analysis," spans a genuinely diverse range of mathematics.

The three-corpus structure also enables capability diagnosis that a single aggregate number would obscure. Consider the paper's own results: DeepHOL achieves 38.9% on complex (validation set, Table 2) and 37.0% on flyspeck (a 2000-theorem sample). These numbers are similar, suggesting that the prover's capabilities transfer across mathematical domains—this would not be diagnosable if the benchmark only provided a single corpus. In future work, a researcher might discover that their new architecture dramatically improves complex performance but degrades on flyspeck; the stratified benchmark would catch this regression, whereas a single aggregate metric might show no change or a small improvement.

The benchmark also constrains the evaluation protocol to prevent information leakage: subgoals inherit the split of their parent theorem, and the validation and test sets are explicitly separated with different recommended usage frequencies ("continuous monitoring" vs. "only used extremely rarely for final assessment"). This attention to evaluation hygiene—specifying exactly how the splits should be used, not just how they are constructed—is unusual for a systems paper and reflects the paper's commitment to creating a benchmark that can actually measure progress over time.

5. Experimental Analysis

Evaluation Methodology

• Dataset. The evaluation uses three corpora derived from the HOL Light proof library and the Flyspeck formalization of the Kepler conjecture. The "core" corpus contains 2,320 theorems covering foundational higher-order logic, the "complex" corpus contains 16,623 theorems from complex analysis, and the "flyspeck" corpus contains 10,519 theorems spanning measure theory, linear algebra, and multivariate analysis (Table 1). Together these comprise 29,462 theorems and lemmas. For model training and evaluation, top-level theorems are split 60:20:20 into training, validation, and test sets, with all subgoals from a theorem's proof inheriting the same split as their parent theorem to prevent information leakage across splits (Section 4.2).

• Base model(s). The primary learned components use WaveNet-based architectures (Van Den Oord et al., 2016) with varying depth and width configurations. The base configuration uses "two WaveNet blocks of four layers each" with 128 or 256 filters per layer (Section 6.2); the deeper variant uses four blocks of five layers each at depth 128, totaling 47 million parameters. The paper also reports results for HOL Light's built-in first-order theorem prover ASM_MESON_TAC as a non-learned baseline. No pretrained language models or external knowledge sources are used—all learning is from the HOList theorem corpus and proof logs.

• Metrics. The primary metric is proof closure rate: the percentage of theorems in a given corpus for which DeepHOL successfully finds a complete, verified proof within the search budget and timeout constraints. This is an end-to-end performance measure, not a proxy. The paper also reports two proxy metrics during model development: (1) accuracy of tactic prediction among the 41 possible tactics (reported as "ranging between 38% and 42% for most models"), and (2) success rate of selecting the correct tactic argument over a randomly chosen negative argument (reported as "around 1% error rate"). All reported proof closures pass through the proof checker that replays the discovered proof through HOL Light's trusted core, ensuring that success rates reflect only logically valid proofs (Section 3.6).

• Baselines. The paper establishes two trivial baselines (Table 2, first two rows):

  • ASM_MESON_TAC (empty arguments): calling HOL Light's built-in first-order prover on each theorem with an empty argument list, achieving 6.1% on the complex validation set. This represents the prover's native capability without learned premise selection.
  • ASM_MESON_TAC + argument selection: calling ASM_MESON_TAC with an argument list predicted by the baseline WaveNet model, achieving 9.2% on the complex validation set. This represents the combination of a classical ATP with learned premise filtering.
  • Supervised WaveNet models in three configurations: a base WaveNet (31.72%), a deeper variant (32.65%), and a wider variant (27.60%), all trained purely by imitation learning on human proof logs without reinforcement learning (Table 2, middle section).

• Generation budget / compute accounting. The paper measures compute through search constraints rather than FLOPs. Each proof attempt is bounded by three limits: (1) a maximum of 100 explored proof states in the proof search graph (the "computation limit"), (2) a total wall-clock timeout of 300 seconds per theorem, and (3) a per-tactic-application timeout of 5 seconds (Section 6.3). These limits apply uniformly across all methods. During reinforcement learning, each round samples 2000 theorems from the training set and distributes proof attempts across 1000 CPU cores. The search hyperparameters (number of top tactics explored, maximum successful applications, argument list length) are randomized per attempt within the ranges specified in Table 3 to increase proof diversity. Model training runs on a single GPU continuously, with checkpoints fetched by prover workers at the start of each round.

• Cross-validation / statistical protocol. The paper does not employ k-fold cross-validation in the traditional ML sense but implements a strict train/validation/test separation protocol (Section 4.2). The validation set "can be used for continuous monitoring for proxy metrics of the model during training" and "is also occasionally used to measure the end-to-end prover performance of the models during training." The test set "must only be used extremely rarely for final assessment of a few models before publishing a paper alongside their validation set performance." The paper reports both validation and test set performance "for the final result to verify that we did not over-fit on the validation set," though the primary results in Table 2 are reported on the validation split of the complex corpus (3,225 theorems). For the Flyspeck corpus, results are reported on a sample of 2,000 proofs rather than the full corpus, likely due to computational constraints.

Main Quantitative Results

Supervised (Imitation) Learning Results

The supervised learning experiments establish the baseline capability of learning to predict human proof steps from the proof logs. All results in this section refer to the complex corpus validation set (Table 2).

The ASM_MESON_TAC baselines are weak but instructive. The built-in first-order prover with empty arguments closes only 6.1% of theorems. Adding the WaveNet-predicted argument list improves this to 9.2%, demonstrating that even a relatively shallow learned premise selector can meaningfully improve a classical ATP's performance by providing it with relevant axioms to work with. However, the absolute numbers are low—the vast majority of theorems in the complex corpus are beyond the reach of first-order automated reasoning, even with premise guidance, confirming that higher-order interactive tactics are necessary for this benchmark.

WaveNet architectures achieve substantially higher closure rates, with depth mattering more than width. The base WaveNet configuration (two blocks of four layers, 128 filters) achieves 31.72% closure. The wider variant with 256 filters per layer actually performs worse at 27.60%, suggesting that the additional capacity leads to overfitting given the available training data. The deeper variant (four blocks of five layers, 128 filters, 47M parameters) achieves 32.65%, a modest but consistent improvement over the base configuration. This pattern—depth helping, width hurting—is consistent with the hypothesis that the hierarchical structure of S-expressions benefits from deeper processing with progressively larger receptive fields, while wider layers simply add parameters without better inductive bias.

The absolute numbers establish the supervised ceiling. Even the best supervised model closes fewer than one-third of the theorems in the complex validation set. This is not a failure of the approach—it reflects the inherent difficulty of theorem proving: at each step of a human proof, there may be multiple alternative valid next steps, and the supervised model only learns to mimic the one the human actually took. When the model deviates from the human path (due to prediction error, or because it explores a tactic the human did not use), it enters proof states for which it has no training examples, and its performance degrades. The gap between supervised learning (~32%) and the RL results (~39%) quantifies exactly how much is lost by restricting to imitation of a single proof strategy.

Reinforcement Learning Results

The RL experiments are the paper's main quantitative contribution, demonstrating that self-generated proof traces can push performance beyond the imitation learning ceiling. All results refer to the complex corpus validation set unless otherwise noted (Table 2, bottom section).

The tactic-independent loop ("Loop") achieves 36.3%, a 4.6 percentage point improvement over the best supervised model (32.65%). This loop used the same base WaveNet architecture as the supervised models, but with continuous RL training where the model's own successful proofs were mixed into the training batches alongside human examples. The training pool configuration comprised human seed examples, inherited computer-generated examples (from a prior supervised model run on the full training set), fresh loop examples (from the last k rounds), and historical loop examples (from earlier rounds), mixed at a fixed ratio to prevent distribution drift. This 36.3% represents the aggregate performance of the final checkpoint from this loop configuration.

The "Trained on loop output" model achieves 36.8%, marginally higher than the loop model itself. This is a separate model that was trained in parallel to the loop, consuming the same training data (mixed from human, inherited, fresh, and historical pools) but not used to guide proof search during the loop. It is, in essence, a model that benefits from the curriculum provided by the loop's proof generation without being subject to the distributional shift of having its own predictions fed back into training. The fact that it performs slightly better than the loop model (36.8% vs. 36.3%) suggests that the loop model may suffer from mild instability—the very fact of using a model's own outputs to guide search and then training on the results can create feedback loops that slightly degrade performance. The "trained on loop output" model avoids this by being a passive beneficiary of the loop's exploration.

The tactic-dependent loop ("Loop tactic dependent") achieves 38.9%, the best overall result. This configuration modifies the neural architecture so that the premise ranking head takes the tactic identity as an additional input: r(t_i) = C(G(g), P(t_i), T_j) rather than r(t_i) = C(G(g), P(t_i)). This allows the model to learn that the same premise theorem may be highly relevant for one tactic (e.g., REWRITE_TAC which applies equational rewrites) but useless for another (e.g., MESON_TAC which performs first-order reasoning). The 2.1 percentage point improvement over the tactic-independent loop (38.9% vs. 36.8% for the comparable "trained on loop output" model) confirms that premise relevance is meaningfully tactic-dependent in this benchmark.

All RL configurations substantially outperform the best supervised WaveNet (32.65%). The improvement ranges from +3.65 percentage points (Loop, 36.3%) to +6.25 percentage points (Loop tactic dependent, 38.9%). Relative to the supervised ceiling, this represents a 11–19% relative improvement. This is the paper's key empirical claim: RL from self-generated proofs provides gains beyond what imitation learning can achieve, and these gains are robust across loop configurations.

The Loop on Subgoals experiment ("Loop on subgoals") is a negative result. This variant modified the proof search to target not just top-level theorems but any internal proof state from the training set, motivated by prior work on curriculum learning and subgoal-based proof strategies (Zombori et al., 2019 [50]). The paper reports this experiment implicitly—it does not appear in Table 2's main results, and the text states that "our naive implementation did not seem to end up with improved results." Table 4 provides context: the subgoal loop found 1,988 proofs (19.5% of the training set) compared to 5,679 (55.7%) for the main loop. This negative result suggests that training on all subgoals indiscriminately may dilute the training signal—subgoals from failed proof attempts may not be meaningfully "provable" in isolation, and the model may waste capacity learning to predict actions for subgoals that are dead ends.

Proof Discovery During Training

The paper provides two figures tracking the RL loop's behavior over time, both reporting on the training set (not validation set, since validation performance was not tracked continuously due to computational cost).

Cumulative proofs discovered (Figure 2, "tactic dependent loop"). This figure shows the cumulative number of distinct theorems from the training set (10,199 theorems total in the joined core+complex training split) for which at least one proof was found by any round of the loop. The curve rises with each round, asymptotically approaching a total of approximately 5,500–6,000 theorems proved. Table 4 confirms the final count: 5,518 theorems proved (54.1% of the training set). This cumulative metric measures the loop's exploration breadth—how many distinct theorems the prover can eventually prove across all rounds, even if not all are proved in every round.

Per-round success rate (Figure 3). This figure shows the percentage of the 2,000 sampled theorems that were successfully proved in each individual round. The metric fluctuates around a central tendency rather than showing a clear monotonic trend. This is expected given the randomized search parameters and the sampling of different theorems each round. The absence of a clear upward trend suggests that the RL training reaches a relatively stable equilibrium quickly, and further rounds primarily maintain performance rather than dramatically improving it. This is consistent with the modest gap between the first loop experiment (36.3%) and the later tactic-dependent variant (38.9%)—the RL process refines rather than revolutionizes the model's capabilities.

The union of all loops proves 5,919 theorems (58.0% of training, Table 4). This is the total number of distinct theorems proved by any of the three loop configurations (main loop, tactic-dependent loop, subgoal loop). The fact that this union exceeds any individual loop's count (e.g., 5,679 for the main loop) indicates that different loop configurations discovered proofs for partially non-overlapping sets of theorems—each configuration has its own strengths and blind spots.

Flyspeck Corpus Results

The "Loop" checkpoint achieves 37.0% on a 2,000-theorem sample from the Flyspeck corpus. This result is reported in a single sentence: "We also ran the final checkpoint of the 'Loop' on a sample of 2000 proofs from the flyspeck dataset; we closed 752 (37.0%) of these proofs automatically." The Flyspeck corpus comprises 10,519 theorems (Table 1) spanning measure theory, polyhedral geometry, linear algebra, and multivariate analysis—mathematical domains substantially different from the complex analysis focus of the complex corpus. The 37.0% closure rate is comparable to the 36.3% achieved by the same model on the complex validation set, suggesting that DeepHOL's learned proof strategies transfer across mathematical domains. However, this result should be interpreted cautiously: (1) it uses only a sample of 2,000 theorems rather than the full corpus, (2) it uses the Loop checkpoint (36.3% on complex) rather than the stronger Loop tactic dependent checkpoint (38.9% on complex), and (3) the Flyspeck corpus was not used during training—the model was trained on core+complex—making this a zero-shot transfer evaluation.

Ablation Studies and Robustness Checks

WaveNet width (filter count): wider degrades performance. The paper reports that the base WaveNet with 128 filters achieves 31.72% while the wider variant with 256 filters achieves only 27.60% (Table 2). This 4.12 percentage point drop from increasing filter count suggests that the model capacity exceeds what the training data supports, leading to overfitting. The deeper variant (more blocks and layers) with 128 filters achieves 32.65%, demonstrating that depth improves representation quality without the overfitting penalty of increased width. This is consistent with the inductive bias hypothesis: deeper dilated convolutions provide exponentially larger receptive fields that match the hierarchical structure of S-expressions, while wider filters simply add parameters that memorize training-set artifacts.

WaveNet depth: deeper improves performance. The deeper configuration (four blocks of five layers, 47M parameters) achieves 32.65% vs. 31.72% for the base configuration (two blocks of four layers). The improvement is modest (+0.93 percentage points) but consistent. The paper does not explore deeper configurations beyond this point, so it is unknown whether the trend continues or plateaus.

Tactic-conditioned vs. tactic-independent premise scoring: conditioning helps. The Loop tactic dependent experiment (38.9%) outperforms both the Loop experiment (36.3%, tactic-independent) and the Trained on loop output experiment (36.8%, also tactic-independent). The 2.1–2.6 percentage point gap is the cleanest comparison because all three configurations share the same base WaveNet architecture and training data sources. This ablation confirms that premise utility is meaningfully tactic-specific—a theorem that rewrites a + b = b + a is relevant when the tactic is REWRITE_TAC but irrelevant when the tactic is MP_TAC (which performs modus ponens).

Reinforcement learning vs. pure supervised learning: RL provides substantial gains. Across all RL configurations, the minimum RL performance is 36.3% (Loop) compared to 32.65% for the best supervised model (Deeper WaveNet). This +3.65 percentage point floor quantifies the minimum benefit of RL. The maximum benefit is +6.25 percentage points (Loop tactic dependent vs. Deeper WaveNet). Since all models use the same WaveNet architecture, the improvement is attributable to the training methodology (RL with self-generated examples) rather than architectural changes.

Training on loop output without participating in the loop: comparable or slightly better. The Trained on loop output model achieves 36.8%, slightly exceeding the Loop model's 36.3%. This is a robustness check on the RL feedback loop itself: it suggests that the primary benefit of RL comes from the expanded and diversified training data (proofs discovered by the loop) rather than from the specific mechanism of using the continuously-updating model to guide search. The slight underperformance of the loop model relative to the passively-trained model may indicate a subtle form of instability: using a model to guide search while simultaneously training it on the results can create a feedback loop where the model's biases in proof search become self-reinforcing in the training data.

Loop on subgoals: a negative result. The attempt to train on all subgoals rather than only top-level theorems "did not seem to end up with improved results." Table 4 quantifies this: the subgoal loop found proofs for only 1,988 theorems (19.5% of training) vs. 5,679 (55.7%) for the main loop. The paper hypothesizes that training on arbitrary subgoals may be counterproductive because not all subgoals are independently provable. However, the experimental design confounds two variables: training on subgoals vs. modifying which goals the proof search targets. It is possible that the subgoal loop's poor performance stems from the proof search modification rather than from the training on subgoals, but the paper does not isolate these effects.

Randomized search parameters: not ablated directly, but integral to the loop design. The paper does not report an ablation where search parameters are held fixed (e.g., always explore exactly 6 tactics, always use 3 successful applications, always use 16 arguments). Without this ablation, it is not possible to attribute any specific fraction of the RL improvement to the randomization itself vs. the continuous training methodology. However, the authors clearly believe the randomization is important, as they specify the ranges in Table 3 and motivate them explicitly: "to increase the diversity of the generated proofs. This also increases the chance of finding a proof at all for harder statements."

Seeded vs. unseeded RL: not fully ablated. The paper states that "preliminary experiments have shown that, in its current form, it learns inferior models compared to those that were seeded with human proofs," but no quantitative results are reported for unseeded RL. This is a significant missing ablation—without knowing the magnitude of the gap between seeded and unseeded RL, we cannot assess how dependent the system is on human demonstrations vs. what it could eventually learn through pure exploration given sufficient compute. The paper acknowledges this as a preliminary finding and does not claim it as a robust result.

Proof pruning: not ablated directly. The paper describes the proof pruning procedure in Section 5.6.1 but does not report an experiment comparing RL with and without pruning. The quality of the training data (whether argument lists contain superfluous theorems) likely affects the premise ranking model's accuracy, but the magnitude of this effect is unknown.

Critical Assessment

Claim 1 from the Executive Summary: "DeepHOL closes 38.9% of validation theorems in the best loop configuration, substantially surpassing a trivial baseline (9.2%) and a purely supervised WaveNet model (31.72%)." This claim is directly supported by Table 2, and the numbers are unambiguous. The trivial baselines (6.1% and 9.2%) are indeed trivial—no reasonable person would argue that a 6% closure rate represents a competitive prover. The supervised WaveNet baseline (31.72%) represents a meaningful comparison because it uses the identical neural architecture, differing only in training methodology. The 7.18 percentage point gap between best supervised and best RL is substantial in absolute terms and represents a ~22% relative improvement.

However, there is a subtlety: the best supervised model (Deeper WaveNet, 32.65%) uses a different architecture (four blocks of five layers) than the RL models (two blocks of four layers). The paper states that "the reinforcement learning experiments was performed earlier and was ran with the narrow architecture." This means the RL improvement is partially confounded with architecture—we cannot be certain how much of the gap would remain if the RL experiments used the deeper WaveNet architecture. It is possible that supervised deeper WaveNet + RL would achieve even more than 38.9%, or that the deeper architecture would provide diminishing returns in the RL setting. The paper's claim of "substantially surpassing" is correct, but the exact magnitude of the RL benefit is subject to this confound.

Claim 2: "reinforcement learning from self-generated proof traces meaningfully improves over imitation learning alone." This claim is well-supported by the comparison between RL configurations (36.3–38.9%) and supervised configurations (27.60–32.65%). The improvement is consistent across loop variants, and the gap persists when comparing the most directly comparable architectures (base WaveNet: 31.72% supervised vs. 36.3% Loop). The mechanism—self-generated proofs expanding the training distribution beyond what humans wrote—is plausible and consistent with the literature on iterative self-improvement in RL.

A weakness is that the paper does not disentangle which aspect of RL is responsible for the improvement. The RL loop differs from supervised training in at least four ways: (1) more total training data (human + self-generated vs. human only), (2) different data distribution (including proof paths humans didn't take), (3) continuous training with fresh examples, and (4) model self-play (using the model's own predictions to guide search). The "Trained on loop output" experiment (36.8%) isolates factors (1) and (2) from (4), showing that most of the benefit comes from the expanded training data rather than from the self-play dynamics. But the remaining 2.1 percentage points between 36.8% and 38.9% might come from architecture (tactic-dependent vs. independent scoring) rather than from training methodology. Without a tactic-dependent model trained purely on loop output, we cannot be certain.

Claim 3: "the system remains bounded to proofs within the scope of the available tactic and premise libraries, as the hardest theorems in the Flyspeck formalization yield lower closure rates (37.0%)." This claim is somewhat misleading as stated. 37.0% on Flyspeck is not "lower" in a meaningful sense—it is essentially identical to the 36.3% achieved by the same model on the complex validation set. The paper itself does not make the claim that Flyspeck theorems are "harder"; Table 2 and the Flyspeck result use different models (Loop not Loop tactic dependent) and different evaluation protocols (validation set vs. sample), making direct comparison unreliable. Furthermore, the paper does not provide difficulty-stratified results—we do not know whether the specific Flyspeck theorems that were proved were the easier ones or were representative.

The more accurate characterization would be: the system achieves comparable closure rates on the complex and flyspeck corpora (~36–37%), suggesting that its learned strategies transfer across mathematical domains, but the absolute closure rate of ~37% means that the majority of theorems in both corpora remain unproved. The "boundedness" claim is correct—no configuration exceeds 38.9%, and Figure 2 shows asymptotic behavior in cumulative proofs discovered—but the paper does not diagnose why the remaining ~60% are unproved. Is it because the WaveNet architecture lacks capacity? Because the 41-tactic set is insufficient to express the necessary proof steps? Because the search budget (100 states, 300 seconds) is insufficient? Because the RL training has not yet converged? Without this diagnosis, the "boundedness" is an observation rather than an explanation.

Missing experiments that would strengthen the paper:

• No comparison to non-neural ATP systems with premise selection. The paper cites extensive prior work on premise selection for first-order ATPs (Kaliszyk and Urban [17], [18]) but does not run these systems on the HOList benchmark as baselines. The only non-neural baseline is ASM_MESON_TAC with empty arguments (6.1%) or WaveNet-predicted arguments (9.2%). A baseline using, e.g., k-nearest-neighbor premise selection (as in TacticToe [9] or the Mizar work [13]) with ASM_MESON_TAC would establish whether the neural approach outperforms traditional ML for premise selection on this benchmark. The paper's argument that prior systems operate on different provers and corpora is valid for precluding direct comparison, but implementing a simple non-neural baseline within HOList would be straightforward and highly informative.

• No per-tactic breakdown of success and failure. The paper reports aggregate tactic prediction accuracy (38–42%) but does not report which tactics are most frequently predicted correctly, which are most frequently confused with each other, or which tactics account for the majority of successful proof closures. This information would be valuable for understanding whether the model has mastered a subset of the tactic repertoire while remaining incompetent at others, or whether its competence is evenly distributed.

• No analysis of proof length, proof shape, or proof novelty. The paper does not report whether the RL-discovered proofs are shorter, longer, or structurally different from the human proofs on the same theorems. This is a missed opportunity: one of the most exciting possibilities of neural theorem proving is discovering proofs that humans missed—either shorter proofs, or proofs using different lemmas, or proofs with different overall architecture. Without this analysis, we do not know whether the RL model is merely reproducing human proof strategies more reliably or actually discovering novel proofs.

• No sensitivity analysis for search budget. The paper uses a fixed budget of 100 proof states and 300 seconds for all RL experiments. There is no experiment showing how performance varies as the search budget increases. If performance plateaus at 50 states, the budget is wasteful; if it continues improving to 500 states, the budget is constraining. Without this analysis, the reported closure rates are specific to the chosen budget and may understate the model's true capability (if it would benefit from more search) or overstate its efficiency (relative to what a simpler method could achieve with more search).

• No experiment varying the size of the human seed data. The paper uses the full human proof logs as seed but states that unseeded RL produces "inferior models." How much human data is necessary? Would 10% of the human proofs suffice? 50%? This is crucial for understanding whether the approach could scale to domains where human proofs are scarce or nonexistent.

• No measurement of the "difficulty estimation cost" analog. In theorem proving, the cost of proof search is the primary compute expenditure, and the paper accounts for it through the 300-second timeout. However, the precomputation of premise embeddings at the start of each round has a computational cost that is not reported. For the 29,462 theorems in the full corpus, encoding all premises through the WaveNet Premise Encoder is potentially substantial (though amortized across the 2,000 theorems attempted in the round). The paper states this precomputation "greatly accelerates" proof search but does not quantify the tradeoff.

Where the claims hold conditionally:

The claim that DeepHOL "demonstrates strong automated reasoning capabilities" holds conditionally: it is strong relative to the trivial baselines and to prior neural theorem provers (Holophrasm's "mostly proofs for very simple theorems"), but it is weak in absolute terms (38.9% leaves 61.1% unproved). The claim that the environment enables "research and measuring progress of AI driven theorem proving in large theories" is well-supported by the paper's infrastructure contributions but the experimental results show that there is substantial room for progress—the benchmark is not saturated.

The claim that the two-tower architecture "is not specialized to [HOL Light]" and "would also work with other goal-tactic based prover like Coq, HOL4, or Lean" is an architectural hypothesis, not an experimental result. The paper does not demonstrate transfer to any other ITP, and the reader should treat this as a design claim rather than an established finding.

6. Limitations and Trade-offs

6.1 The Hardest Theorems Remain Effectively Unsolved — A Hard Capability Ceiling

The constraint. Across all models and training configurations, DeepHOL's proof closure rate on the complex corpus plateaus at 38.9% (Table 2), meaning that over 60% of the benchmark theorems remain unproved. The paper does not break down performance by theorem difficulty, but the aggregate numbers imply a fundamental boundary: there exists a large class of theorems for which the system—regardless of architecture, training methodology, or search budget—cannot find proofs. The paper acknowledges the existence of this ceiling indirectly through the asymptotic behavior of the cumulative proofs curve (Figure 2), which shows the number of distinct theorems proved approaching roughly 5,500–6,000 out of 10,199 training theorems (54–59%, Table 4) and then flattening.

The consequence. This is not merely "the system could be better." It means that for the majority of theorems in the benchmark, the neural prover provides zero value—it cannot find a proof, and a human must still construct the entire proof from scratch. The system does not degrade gracefully on hard theorems (producing partial proofs that a human could complete); it simply fails. This is a hard requirement for any practical deployment of an automated theorem prover: if the system cannot prove the theorem, does it at least make the human's job easier? The paper provides no evidence that DeepHOL's partial proof attempts are useful to humans.

What evidence exists. The paper reports only aggregate closure rates, with no per-theorem difficulty analysis, no stratification by proof depth, and no measurement of how far partial proofs progressed before failing. The gap between the best RL configuration (38.9%) and 100% is a direct quantification of the capability ceiling, but the paper does not diagnose why the remaining theorems are unproved. Are they theorems requiring tactics outside the supported set of 41? Theorems whose proofs are longer than the 100-state search budget allows? Theorems whose necessary premises are not recognized by the premise scorer? Theorems that require creative mathematical insight beyond pattern-matching against the training distribution? Without this diagnosis, the ceiling is a black box—a practitioner cannot predict which of their own theorems will fall on which side of the boundary.

Mitigation status. The paper does not attempt to address this limitation. Section 7 (Conclusion) frames the results as "strong initial results" and positions the benchmark as a platform for future improvement, which implicitly acknowledges the ceiling but offers no concrete direction for breaking through it. The restriction to 41 tactics that take only previously-proved theorems as arguments (Section 3.4) is a deliberate simplification that almost certainly excludes some human-proof strategies; relaxing this restriction could expand the set of provable theorems but would fundamentally change the action space, requiring the model to generate arbitrary HOL terms rather than selecting from a finite library—a much harder learning problem.

6.2 The Difficulty Estimation Cost Is Unaccounted for in Headline Performance

The constraint. DeepHOL's reinforcement learning loop precomputes premise embeddings for all theorems in the library at the start of each round: "At the start of each round, we fetch the latest trained model checkpoint and precompute the theorem argument embedding for each theorem in the complex and core libraries. This precomputation greatly accelerates the ranking of the tactic arguments" (Section 6.3). For a library of 29,462 theorems, this means running the full WaveNet Premise Encoder on every theorem before a single proof search can begin. The paper does not report the computational cost of this precomputation, nor does it account for it in the reported performance metrics or the 300-second per-theorem timeout.

The consequence. The headline 38.9% closure rate is achieved under a cost model that omits a substantial fixed overhead. In a deployment scenario where a user submits a single theorem to be proved, the total time would be precomputation_time + proof_search_time. If precomputation takes, say, 10 minutes for 30K theorems (a plausible estimate given that a forward pass through a 47M-parameter WaveNet on 30K inputs of ~500 tokens each is non-trivial), then the total cost per theorem is dominated by the fixed overhead, making the system impractical for interactive use. Even in the batch setting used in the paper (2,000 theorems per round), the precomputation cost is amortized across 2,000 theorems—the 38.9% figure reflects this amortized setting, not the per-theorem cost a practitioner would experience.

What evidence exists. The paper provides no measurement of precomputation time, no FLOP accounting, and no comparison of total compute (including precomputation) against alternative approaches. The statement that precomputation "greatly accelerates" proof search is true but one-sided—it accelerates search given that the precomputation has already been done, but it does not account for whether the total end-to-end time (including precomputation) is competitive with alternatives that compute premise embeddings on-the-fly or use cheaper premise selection methods.

Mitigation status. The paper does not address this issue. The precomputation is presented as an optimization, not as a cost to be accounted for. No ablation studies whether on-the-fly computation (possibly with a smaller, cached subset of premises) would be competitive. The paper also does not explore incremental precomputation (only updating embeddings for theorems whose representations have changed due to training), which could reduce the per-round cost.

6.3 Single Benchmark, Single Prover, Single Model Family — No Evidence of Generality

The constraint. Every experiment in the paper uses exactly one interactive theorem prover (HOL Light), one benchmark (the HOList corpus derived from HOL Light's standard library and the Flyspeck formalization), one model architecture family (WaveNet), and one base model training paradigm (supervised pretraining on human proofs followed by RL). The paper makes architectural claims of generality—"We believe that our solution would also work with other goal-tactic based prover like Coq, HOL4, or Lean" (Section 5)—but provides no empirical evidence for this belief.

The consequence. A practitioner using a different ITP (Coq, Isabelle, Lean) cannot assume that DeepHOL's design decisions will transfer. Different ITPs have different tactic languages (Coq's Ltac vs. HOL Light's OCaml-level tactics), different logical foundations (calculus of inductive constructions vs. classical higher-order logic), different theorem library organizations, and different proof styles. The restriction to 41 tactics in HOList is specific to HOL Light; Coq has a much richer and more extensible tactic language. The S-expression representation is specific to HOL Light's term structure; Coq's terms include dependent types and universe levels that would require a different encoding. The paper provides no analysis of which aspects of the architecture are ITP-agnostic vs. ITP-specific, making it impossible for a practitioner to assess the porting effort.

Furthermore, the claim that PaLM 2-S* (in the reference example used as template) is "representative" is not the claim here—the issue is that WaveNet is the only architecture tested. The paper does not compare against transformers, RNNs, or graph neural networks on the same benchmark, so there is no evidence that WaveNet's inductive biases (dilated convolutions, exponentially growing receptive field) are actually beneficial for S-expression encoding rather than merely adequate. The supervised architecture comparison in Table 2 varies only WaveNet hyperparameters (depth, width), not the fundamental model class.

What evidence exists. The results in Table 2 are exclusively from WaveNet variants. The paper's only cross-domain evidence is the single Flyspeck sample result (37.0% on 2,000 theorems using the Loop checkpoint, Section 6.3), which is within the same ITP (HOL Light) and uses a corpus derived from the same formalization effort (Flyspeck). This is weak evidence for generality—the Flyspeck and complex corpora share the same logical foundations, tactic set, and proof conventions because they are both part of the same HOL Light library.

Mitigation status. The paper does not address this limitation. The generality claim is presented as a belief, not an experimental finding. No experiments are proposed for future work that would test transfer to other ITPs, and the paper does not discuss what modifications would be necessary to port DeepHOL to Coq or Isabelle.

6.4 The 38.9% Result Is Architecture-Confounded — RL vs. Supervised Comparison Uses Different WaveNet Configurations

The constraint. The paper's headline comparison—RL beats supervised learning—is confounded by architecture. The supervised learning experiments use three WaveNet configurations (Section 6.2), with the best being the Deeper WaveNet: "four blocks of five layers each, in this case with depth 128... which has 47 million parameters." The RL experiments, however, use a different configuration: "the reinforcement learning experiments was performed earlier and was ran with the narrow architecture (with 128 filters in each layer) and with two wavenet blocks" (Section 6.2). This means the RL models have fewer layers (2 blocks × 4 layers = 8 layers vs. 4 blocks × 5 layers = 20 layers) and substantially fewer parameters than the best supervised model.

The consequence. The reported gap between the best RL result (Loop tactic dependent: 38.9%) and the best supervised result (Deeper WaveNet: 32.65%) conflates two effects: the benefit of RL training and the detriment of using a smaller architecture. If the RL loop had been run with the deeper WaveNet architecture, would the performance be higher than 38.9% (because more capacity + RL > less capacity + RL)? Or would it be similar (because RL benefits saturate even with shallower architectures)? Or would it be lower (because the larger model requires more data to train effectively in the RL setting)? The paper provides no evidence to answer these questions.

This confound also affects the comparison between Loop configurations. The tactic-dependent loop (38.9%) uses a different combiner architecture than the tactic-independent loop (36.3%), but both use the same base WaveNet. It is unclear whether the 2.6 percentage point gain comes from tactic conditioning specifically or from the increased model capacity in the combiner (since the tactic-dependent combiner takes [goal_embedding, premise_embedding, tactic_embedding] rather than [goal_embedding, premise_embedding]).

What evidence exists. The paper explicitly acknowledges the architecture difference: "Note that the reinforcement learning experiments was performed earlier and was ran with the narrow architecture" (Section 6.2). This is an honest disclosure, but it does not resolve the confound. The paper reports no experiment that holds architecture constant while varying only training methodology, which is the standard ablation required to isolate the RL effect.

Mitigation status. The paper acknowledges the confound but does not resolve it. The "Trained on loop output" experiment (36.8%) uses the same narrow WaveNet as the Loop experiments, making it a cleaner comparison to the supervised narrow WaveNet (not reported separately—the 31.72% base WaveNet in Table 2 uses 128 filters and two blocks, which likely matches). This suggests the RL benefit over architecture-matched supervised training is approximately 36.8% - 31.72% = 5.08 percentage points. However, this comparison is not highlighted in the paper, and the "Trained on loop output" model is described as "a separate model that was not used in the loop for proof search guidance" (Section 6.3), making it a slightly different training setup than the main supervised models.

6.5 No Analysis of Whether Discovered Proofs Are Novel or Merely Reproductions

The constraint. The paper evaluates DeepHOL exclusively by whether it can prove a theorem (binary success/failure), with no analysis of the characteristics of the proofs it discovers. Specifically, the paper does not report whether the RL-discovered proofs differ from the human proofs in the training corpus in terms of length (number of tactics applied), lemma usage (which premises are invoked), or overall proof structure (the shape of the proof tree). The paper's proof logging infrastructure records the entire proof tree (Section 3.3), so this data is available but not analyzed.

The consequence. This is a significant gap for interpreting what the RL loop actually learns. There are two very different success modes for RL in theorem proving:

1. Reproduction mode: The RL model learns to more reliably reproduce the human proof strategies that were already present in the training data. The 38.9% closure rate would represent theorems where the human proof is within the model's search scope, and RL has improved the model's ability to stay on the human path.

2. Discovery mode: The RL model discovers proofs that are qualitatively different from the human proofs—shorter, using different lemmas, or with entirely different structure. The 38.9% closure rate would include some theorems that the human proof logs did not cover (or covered with a proof the model couldn't reproduce), but which the model found through alternative reasoning paths.

The paper's framing—"improves itself using reinforcement learning" (Section 1)—implies discovery mode. But without proof analysis, we cannot distinguish these modes. If the RL model is merely better at reproducing human proofs (mode 1), it is an incremental improvement in search reliability, not a qualitatively new capability. If it is discovering novel proofs (mode 2), it represents a genuinely different kind of theorem proving.

What evidence exists. The paper provides no proof-level analysis. The only structural metric reported is the cumulative number of distinct theorems proved (Table 4, Figure 2), which speaks to coverage breadth but not to proof novelty. The paper's unsupported claim that DeepHOL's "intelligence is fully learned without any hand-crafted features, and with very simple data preprocessing" (Section 5) is not evidence of novel proof discovery—a model can learn to reproduce human patterns without hand-crafted features.

Mitigation status. The paper does not address this limitation. The proof trees are serialized and stored (Section 5.3), so the data exists for future analysis, but the paper provides no tools, metrics, or methodology for comparing discovered proofs against human proofs. This is a missed opportunity because the HOList environment is uniquely positioned to enable exactly this kind of analysis—it has both the human proof corpus and a mechanism for replaying proofs through the trusted kernel—but the paper's experimental reporting does not exploit this capability.

6.6 The Search Budget Is Fixed and Uninformed — No Adaptation to Theorem Difficulty

The constraint. Every theorem in the benchmark receives the identical search budget: a maximum of 100 explored proof states and a total timeout of 300 seconds (Section 6.3). The proof search algorithm is a simple breadth-first search with no mechanism for allocating more resources to promising branches or fewer to dead ends. The Action Generator scores tactics and premises, but these scores are used only for ordering within a single goal expansion, not for global resource allocation across the proof search graph. The paper does not implement best-first search, iterative deepening, or any form of Monte Carlo tree search that could dynamically allocate computation.

The consequence. The fixed budget creates a rigid cost structure where easy theorems (which might be provable in 5 states and 10 seconds) receive the same maximum allocation as hard theorems (which might require the full 100 states and 300 seconds and still fail). This is both inefficient (wasting compute on easy theorems that could be solved faster) and potentially capability-limiting (hard theorems that would be provable with 200 states and 600 seconds are abandoned prematurely). The paper's results therefore reflect a specific, arbitrary cost-performance tradeoff; a different budget might yield different closure rates and different relative rankings between methods.

More subtly, the fixed budget means the RL training signal is coarse. When a proof attempt fails due to timeout or state limit, the system does not know whether the failure was because the theorem is genuinely beyond the model's capability, or because a slightly larger budget would have allowed the proof to complete. This ambiguity contaminates the training data: subgoals from failed proofs are not added to the training pool (since only successful proofs generate training examples, Section 5.6), but the system cannot distinguish between "this subgoal is provable with the current model and a bit more search" and "this subgoal is unprovable."

What evidence exists. The paper does not ablate the search budget. There is no experiment showing how proof closure rate varies with the number of explored states or the timeout duration. The paper also does not report the distribution of actual resource consumption for successful proofs (e.g., median states explored, median wall-clock time), which would indicate how much of the budget is typically used and whether the 100-state limit is binding.

Mitigation status. The paper does not address this limitation. Search budget is treated as a fixed environmental parameter, not as a variable to be studied or optimized. The paper does not propose adaptive budget allocation as a direction for future work, though the framework (the Action Generator provides scores that could, in principle, inform a best-first search) would support it.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper changes the landscape for ML-driven theorem proving by shifting the bottleneck from infrastructure to methodology. Before HOList, a machine learning researcher who wanted to work on higher-order theorem proving faced a multi-month integration challenge: learn the internals of an ITP (HOL Light, Coq, or Isabelle), implement a custom OCaml-Python bridge, design a serialization format for proof states, build a proof search engine from scratch, and only then—after all that engineering—begin to experiment with neural architectures. The paper explicitly frames this barrier:

"The long-term goal is to enable the automatic formalization of large theories, and hence we want to start with a theorem proving system that has a track-record of large-scale formalization efforts."

What HOList provides is not merely a dataset but a stable API contract that decouples the ML research from the ITP internals. The significance of this decoupling is not that it makes the work easier—it is that it makes the work comparable. When two groups report proof closure rates on the HOList benchmark, they are using identical theorem statements, identical tactic semantics, identical premise availability ordering, and identical evaluation splits. This is the same shift that ImageNet enabled for computer vision: before ImageNet, every vision group used their own dataset with their own evaluation protocol, and it was impossible to tell whether a new architecture was genuinely better or merely better-tuned to a particular data distribution. HOList does not solve theorem proving—the 38.9% closure rate makes that clear—but it solves the benchmarking problem, which is a prerequisite for cumulative scientific progress.

The secondary shift is more subtle: the paper demonstrates that reinforcement learning from self-generated proofs is viable at scale for higher-order logic, but only when carefully architected. The continuous mixing of four training pools at fixed ratios, the diversity-enforcing randomization of search parameters, and the proof pruning procedure are each individually small design choices, but together they form a recipe for stable self-improvement that had not been demonstrated before at this scale. Prior RL efforts in theorem proving either used toy logics (Whalen [21], Metamath), or operated in first-order settings with hand-engineered features (Kaliszyk et al. [25]), or did not demonstrate end-to-end proof closure improvements over supervised baselines. The gap between DeepHOL's best supervised result (32.65%) and best RL result (38.9%)—a 19% relative improvement—is the first quantitative evidence that self-generated proof traces can push a neural prover beyond the imitation learning ceiling in a realistic higher-order setting. This reframes the conversation from "can neural networks help with theorem proving?" (answered affirmatively by Alemi et al. [19] and others for premise selection) to "can neural networks teach themselves to prove theorems beyond what humans have demonstrated?"—a substantially more ambitious question that the paper partially answers and leaves open.

The paper also reconciles a tension in prior work between two competing framings of ML for ITPs. One tradition, exemplified by TacticToe [9] and the extensive premise selection literature ([17, 18, 19, 32, 33, 35]), treats machine learning as a retrieval problem: given a proof state, retrieve similar states from a database and reuse their human-chosen actions. This framing works well when the proof corpus is large and the prover's task is to reproduce human strategies. Another tradition, exemplified by Holophrasm [21] and the RL-for-ATP work [25], treats machine learning as a policy learning problem: learn a function from proof states to actions that maximizes the probability of finding a proof, potentially discovering strategies humans never used. These framings seemed incompatible—retrieval methods could not discover novel proofs, and policy learning methods struggled with the exploration problem in combinatorially vast proof spaces. DeepHOL's architecture shows they are complementary: the supervised pretraining phase (imitating human proof logs) solves the cold-start problem by giving the policy a reasonable initialization, and the RL phase (self-generated proofs with fixed-ratio mixing) pushes the policy beyond imitation without forgetting the human strategies. The four-pool training mixture is the mechanism that makes this complementarity work in practice.

Directions that become more attractive. The paper makes verifier design the central bottleneck for neural theorem proving, though this is implicit rather than explicit. The proof checker architecture (Section 3.6)—where an untrusted Python search procedure generates candidate proofs and a trusted OCaml kernel verifies them—creates a natural separation of concerns that makes it safe to experiment with aggressive, heuristic, or even buggy search algorithms. This means researchers can focus on improving the generation of candidate proofs without worrying about soundness, because the verifier will reject anything invalid. This is analogous to how the RLHF literature recognized reward model quality as the central challenge—once you have a reliable verifier, you can push the generator arbitrarily hard. The paper does not explore improving the proof verifier (HOL Light's kernel is fixed), but it establishes the architectural pattern that makes verifier-aware research natural.

Directions that become less attractive. The paper's negative result on subgoal-based training (Section 6.3: "our naive implementation did not seem to end up with improved results") and its finding that unseeded RL produces inferior models ("preliminary experiments have shown that, in its current form, it learns inferior models compared to those that were seeded with human proofs") together suggest that purely exploratory RL without demonstration data is not a viable path for theorem proving at this scale. The combinatorics of the proof space are simply too unforgiving—random exploration has negligible probability of discovering a complete proof for any non-trivial theorem, so there is no reward signal to learn from. This means that approaches based on zero-shot exploration or intrinsic motivation (curiosity-driven RL) face an extremely steep challenge in this domain, and research effort is better directed toward methods that leverage existing proof corpora, even if only as a bootstrap.

Follow-Up Research This Work Enables

Transformer-based encoders for S-expression goals and premises. The paper uses WaveNet (dilated convolutions) exclusively, motivated by the hierarchical structure of S-expressions. But transformers with appropriate positional encodings have since been shown to capture hierarchical structure effectively, and they offer the advantage of explicit attention over long-range token dependencies—important when a theorem's relevant premise might be a sub-expression buried 400 tokens into the goal string. A direct comparison on the HOList benchmark would answer: does the choice of sequence encoder matter for theorem proving, or is the overall two-tower architecture the dominant factor? A strong follow-up would train a transformer-based Goal Encoder and Premise Encoder on the identical human proof logs, evaluate both supervised and RL configurations, and report not just aggregate closure rate but also per-proof-depth performance (since transformers' quadratic attention might be especially helpful for long proofs requiring long-range premise matching). The HOList Docker container and proof logging infrastructure make this a matter of swapping the encoder—no ITP engineering required.

Difficulty-adaptive proof search budgets. The paper uses a fixed 100-state, 300-second budget for all theorems, with no mechanism to allocate more resources to promising branches or less to dead ends. A natural extension is to use the Action Generator's confidence scores—the softmax probability of the top-ranked tactic and the Combiner Network's premise scores—as a heuristic for best-first search: expand nodes with high predicted provability first, and allocate budget dynamically. This would address both the inefficiency (easy theorems solved in 5 states waste 95 states of budget) and the capability ceiling (hard theorems that are provable with 200 states are abandoned at 100). A strong experiment would: (1) train the Action Generator with an additional value head that predicts "will this goal eventually be proved?" (trained on the outcomes of proof search), (2) implement best-first search ordering nodes by this value estimate, (3) measure proof closure rate vs. total states explored, and (4) report the distribution of states used for successful proofs under adaptive vs. fixed budgets. The HOList environment already records the full proof search graph (Section 5.2), making outcome labels available for value function training.

Cross-ITP transfer: does DeepHOL's architecture work for Coq? The paper claims genericity ("We believe that our solution would also work with other goal-tactic based prover like Coq, HOL4, or Lean"), but provides zero evidence. A high-value follow-up would port the HOList infrastructure to Coq—specifically, instrument Coq to expose the same two-function API (stateless tactic application, theorem registration with fingerprints), export the Coq standard library as normalized S-expressions, and train a two-tower WaveNet (or transformer) on human Coq proof logs. The experiment would measure: (1) Does the same architecture achieve non-trivial closure rates on a comparably-sized Coq corpus without Coq-specific modifications? (2) Do the relative benefits of RL over supervised learning replicate? (3) Are there Coq-specific phenomena (dependent types, richer tactic language) that break the architecture? This is a substantial engineering effort but would transform HOList from a HOL Light-specific benchmark into a general framework for ITP-agnostic neural theorem proving, validating or refuting the paper's central claim of generality.

Proof novelty analysis: do RL-discovered proofs differ from human proofs? The paper's most intriguing possibility—that RL discovers proofs humans didn't write—is entirely unevaluated. A direct follow-up would compare the proof trees generated by the RL loop against the human proof trees for the same theorems, measuring: (1) length ratio (RL proof steps / human proof steps), (2) premise overlap (Jaccard similarity between the sets of theorems used as arguments), (3) structural edit distance between proof trees, and (4) the existence of RL-discovered proofs for theorems where the human proof is not in the training set (because the theorem is in the validation or test split). Finding (4) would be the strongest evidence of genuine proof discovery, while finding only reproductions would reframe DeepHOL as a search amplifier rather than a proof innovator. The serialized proof trees are already stored by the infrastructure (Section 5.3), making this analysis purely a matter of writing the comparison code.

Scaling laws for neural theorem proving: how does performance scale with model size, data size, and search budget? The paper uses a single model scale (~47M parameters for the deeper WaveNet, fewer for the RL configurations) and a single training data scale (all human proof logs from core+complex). A scaling study would train models across an order of magnitude in parameter count (e.g., 10M, 50M, 200M parameters) on varying fractions of the human proof corpus (10%, 25%, 50%, 100%), and measure proof closure rate as a function of both variables. The key question is whether theorem proving exhibits the same power-law scaling as language modeling (where performance improves predictably with compute), or whether there are "capability thresholds" where a certain model size suddenly unlocks the ability to prove theorems of a given depth or complexity. The HOList benchmark's three-corpus structure (core, complex, flyspeck) provides natural difficulty strata for measuring whether scaling benefits transfer across mathematical domains or are domain-specific. This would establish the first scaling laws for neural higher-order theorem proving, analogous to what Kaplan et al. (2020) and Hoffmann et al. (2022) did for language modeling.

Negative result stress-test: how much human data is actually necessary? The paper reports that unseeded RL learns "inferior models" but provides no quantification. A precise follow-up would vary the fraction of human proof logs used for supervised pretraining—0% (pure RL from scratch), 1%, 5%, 10%, 25%, 50%, 100%—and measure the final RL performance for each. This would answer: is there a sharp phase transition where a small amount of human data unlocks RL's ability to self-improve, or does performance improve smoothly with more seed data? If 5% of human proofs achieves 90% of the full-data RL performance, the approach is much more scalable to new domains than if 80% is required. This experiment directly addresses the bottleneck the paper identifies—dependence on human proof logs—and would tell practitioners how much human effort is needed to bootstrap a neural prover on a new mathematical library.

Practical Applications and Downstream Use Cases

Batch proof automation for formalization projects. The most direct application is using DeepHOL (or a successor trained on the HOList benchmark) to automate the routine lemmas in large-scale formalization efforts. The Flyspeck formalization of the Kepler conjecture required "over 20 person-years" of human effort, much of it spent on lemmas that are mathematically uninteresting but technically necessary—commutativity of addition for matrices, basic properties of set operations, simple epsilon-delta manipulations. The paper's result that DeepHOL closes 37.0% of a Flyspeck sample (752 of 2,000 theorems, Section 6.3) suggests that a significant fraction of these lemmas could be automated. In a practical workflow, a human formalizer would state a lemma, and DeepHOL would attempt to prove it automatically within a fixed time budget (the 300-second timeout from the paper). For the ~37% of lemmas where it succeeds, the human saves time; for the remainder, the human writes the proof manually. Even at the 38.9% closure rate on complex, this represents a substantial reduction in human effort for large formalization projects, and the RL loop means the system could improve as it is exposed to more proofs from the specific project.

Premise selection as a service for interactive theorem provers. DeepHOL's two-tower architecture (Goal Encoder + Premise Encoder + Combiner Network) can be deployed as a standalone premise selection tool even without full proof automation. A human user working in HOL Light (or a future port to Coq/Isabelle) would reach a proof state, query the Premise Scorer for the top-20 most relevant theorems given the current goal, and see a ranked list of potentially useful lemmas. The paper's reported premise selection error rate of "around 1%" (Section 6.2) for selecting a positive argument over a random negative suggests the ranking quality is high. This is valuable because a major bottleneck in interactive theorem proving is simply knowing which lemmas exist—the HOL Light library contains 29,462 theorems, and a human cannot memorize them all. A premise suggestion tool trained on HOList would make the library searchable by semantic relevance rather than by keyword, directly addressing the "where is the lemma I need?" problem that consumes substantial human time in formalization.

Curriculum design for mathematics education. The HOList benchmark's three-corpus structure (core: foundational logic, complex: complex analysis, flyspeck: mixed advanced mathematics) and its dependency-ordered theorem listing provide a natural map of mathematical concept prerequisites. A system trained on HOList to predict which premises are needed for which goals implicitly learns the dependency structure of mathematical knowledge—that proving a theorem about contour integrals requires lemmas about limits, which require lemmas about epsilon-delta definitions, which require lemmas about real number arithmetic. An educational application could use the learned premise embeddings to generate personalized curricula: given a student's current knowledge (represented as the set of theorems they've mastered), the system recommends the next theorem to learn as the one whose predicted premises have maximal overlap with the student's known theorems and whose proof is within the student's predicted capability (using the Action Generator's confidence scores as a proxy for difficulty). The paper does not explore this application, but the infrastructure—particularly the theorem dependency graph and the learned premise relevance scores—provides exactly the data needed to build it.

When to Prefer This Method

The paper does not articulate a clear tradeoff against named alternative neural theorem proving systems, nor does it position DeepHOL against a specific competing architecture with measured performance differences. The experimental comparisons are against trivial baselines (ASM_MESON_TAC with empty or learned arguments, achieving 6.1% and 9.2%) and against ablations of its own architecture (supervised vs. RL, narrower vs. deeper WaveNet). The paper's contribution is primarily infrastructure (the HOList environment and benchmark) and a reference architecture (DeepHOL) that demonstrates the benchmark's feasibility, not a method that wins against established competitors on a shared metric. A forced "prefer X when Y" matrix would invent tradeoffs the paper does not establish. The appropriate guidance is: researchers who want to work on neural higher-order theorem proving should use the HOList environment and benchmark as their evaluation platform, because it provides the stable, reproducible, and comparable evaluation that the field previously lacked—regardless of whether they use DeepHOL's architecture or develop entirely different neural provers.