Learned Interventions in Lean 4 grind

# Learned Interventions Inside Lean 4’s grind
Source: [https://arxiv.org/html/2607.22972](https://arxiv.org/html/2607.22972)
###### Abstract

Lean 4’sgrindtactic combines congruence closure,e\-matching, and case\-splitting into a single automated solver, and like any such solver, it relies on hand\-tuned heuristics to decide what to instantiate and where to case\-split\. These heuristics are tempting targets for learning, but there is a catch: becausegrind’s search is non\-monotone, a learned heuristic that helps one proof can break another, and an always\-on replacement usually nets out near zero\. We avoid this by invoking a learned intervention only after stockgrindhas already failed: a failure\-triggered cascade that, by construction, cannot lose a proofgrindalready had\. We apply it to two ofgrind’s internal decisions\. A cost\-awaree\-matchfilter solves slightly more problems and runs about 5% faster\. A lookahead step, proves five theorems it otherwise times out on\. We also report the negative result that motivated the design: across four feature\-based models, statically predicting the correct case split is no better than random, because whether a split explodes is a runtime property that the features do not capture\. Our results suggest that learning within theorem\-proving tactics is most effective as a mechanism for deciding when and how to spend bounded search, backed by a reliable symbolic fallback\.

Lean 4, grind, premise selection, lookahead, theorem proving, machine learning

## 1Introduction

Automated theorem provers increasingly rely on a small number of powerful tactics as their reasoning backends\. This makes the internal search decisions of those tactics a high\-leverage target for learning: improving a single branching, instantiation, or pruning heuristic can affect many downstream proof attempts\. At the same time, these decisions are difficult to learn safely\. A heuristic that appears better locally may change the shape of the symbolic search enough to create new blow\-ups, causing regressions on goals that the original tactic already solved\.

We study this problem withingrind\(Lean FRO,[2024](https://arxiv.org/html/2607.22972#bib.bib1)\), a recent tactic for the Lean 4 proof assistant\(Moura and Ullrich,[2021](https://arxiv.org/html/2607.22972#bib.bib2)\)\. It integrates SMT\-style automation\(Moura and Bjørner,[2008](https://arxiv.org/html/2607.22972#bib.bib4)\)into Lean by combining congruence closure,e\-match\-based lemma instantiation, and case splitting in a single procedure\. Many of its decisions are heuristic: whiche\-matchinstances to keep, which goal to split next, and in what order to explore the resulting cases\. A single proof may involve thousands of such choices, which makesgrinda natural place to ask whether learned guidance can help\.

Most machine\-learning work for interactive theorem proving operates at the level of tactics or proof steps, outlined in[Section2](https://arxiv.org/html/2607.22972#S2)\. We instead look inside one tactic and modify some of its internal choices rather than replacing the tactic itself\. This keeps the original search procedure in the loop: stockgrindprovides both a baseline and a fallback\.

The main complication is thatgrind’s search is non\-monotone\.e\-matching can grow very quickly, so a choice that appears better in the short term may make the overall search worse\. In our experiments, always\-on learned replacements have this character: they solve some goals that stockgrindmisses, but also break goals that stockgrindcan already prove\. We therefore use learning more conservatively\. Rather than trying to predict the right choice from static features, we run a cheap lookahead that is triggered only after stockgrindfails\. This gives a failure\-triggered cascade: stockgrindis tried first, and the intervention is applied only to the goals it leaves open\. As a result, the intervention does not endanger proofs thatgrindalready solves\.

We evaluate this design with working Lean code\. Our implementation includes a cost\-awaree\-matchfilter and a lookahead step that proves some theorems beyond stockgrind\. We also report a negative result: a static model for predicting the next split performs no better than random choice\. The lesson, then, is not that a neural model should replacegrind’s heuristics, but that learning is best used to locate where static choices fail and to steer bounded search behind a symbolic fallback\.

Our main contributions are:

1. 1\.We formulate failure\-triggered learned intervention as a safe deployment pattern for learning inside non\-monotone theorem\-proving tactics\.
2. 2\.We implement two Lean\-native interventions insidegrind: a cost\-awaree\-matchfilter and a bounded lookahead procedure for case splitting\.
3. 3\.We show that these interventions improve theorem\-level performance without sacrificing baseline solves: thee\-matchfilter gives a small speed and success gain on 855 held\-out theorems, while the lookahead cascade rescues five stockgrindtimeouts with zero regressions\.
4. 4\.We show that static feature prediction is insufficient for the rescuable split decisions: four learned policies fail to beat random choice precisely where it matters, suggesting that branch explosion is primarily a dynamic property of the search\.

## 2Related Work

### Learned heuristics in SAT and SMT\.

The choices we study—which goal to branch on and which instantiations to keep—are close to the branching, restart, and instantiation heuristics used in SAT and SMT solvers\. There is a long line of work on learning such heuristics\. NeuroSAT\(Selsamet al\.,[2019](https://arxiv.org/html/2607.22972#bib.bib15)\)learns a solver from single\-bit supervision; Graph\-Q\-SAT\(Kurinet al\.,[2020](https://arxiv.org/html/2607.22972#bib.bib16)\)uses a graph network as a branching policy for CDCL; and FastSMT\(Balunovićet al\.,[2018](https://arxiv.org/html/2607.22972#bib.bib17)\)learns to compose Z3 tactic strategies\. These systems score the current state from its features\. Our split\-rescue experiments suggest that this is not enough for the choices insidegrind: on the high\-impact decisions, static scoring is no better than random choice \([Table1](https://arxiv.org/html/2607.22972#S5.T1)\)\. The issue is that the cost of a branch is often visible only after taking it\. Our positive result therefore uses lookahead rather than a purely static prediction\.

### E\-graphs and equality saturation\.

grindmaintains an e\-graph through congruence closure, the same basic data structure used by equality\-saturation systems such as egg\(Willseyet al\.,[2020](https://arxiv.org/html/2607.22972#bib.bib18)\)\. In those systems, a central problem is controlling e\-graph growth by deciding when to apply rewrite rules\. Oure\-matchfilter addresses a similar problem insidegrind: it tries to discard low\-value instantiations before they are added to the e\-graph\. The failures of this filter are also useful\. The heavy\-tailed, lemma\-diverse explosions described in[AppendixB](https://arxiv.org/html/2607.22972#A2)show why simple pruning rules are not enough to control growth in all cases\.

### Learning for interactive theorem proving\.

Most learning\-based work in interactive theorem proving operates at the level of tactics or proof steps\. Examples include language models that generate proof steps\(Polu and Sutskever,[2020](https://arxiv.org/html/2607.22972#bib.bib7); Yanget al\.,[2023](https://arxiv.org/html/2607.22972#bib.bib9)\), learned tactic policies\(Gauthieret al\.,[2021](https://arxiv.org/html/2607.22972#bib.bib10)\), and neural\-guided proof search\(Lampleet al\.,[2022](https://arxiv.org/html/2607.22972#bib.bib8); Silveret al\.,[2018](https://arxiv.org/html/2607.22972#bib.bib6)\)\. Premise selection and hammer systems instead retrieve useful lemmas for an external prover\(Alemiet al\.,[2016](https://arxiv.org/html/2607.22972#bib.bib11); Blanchetteet al\.,[2016](https://arxiv.org/html/2607.22972#bib.bib12); Czajka and Kaliszyk,[2018](https://arxiv.org/html/2607.22972#bib.bib13)\)\. Our setting is different: we keep the tactic fixed, and learn only some of its internal choices\. This keeps the original symbolic search as the baseline and fallback\.

### Algorithm selection and portfolios\.

Our failure\-triggered cascade is related to algorithm selection and portfolio solvers such as SATzilla\(Xuet al\.,[2008](https://arxiv.org/html/2607.22972#bib.bib19)\)\. Portfolio methods usually pick a solver or configuration up front, based on features of the instance\. Our cascade makes the decision later\. It first runs stockgrind, and invokes the learned procedure only on goals that remain unsolved\. This avoids having to predict in advance whether learning will help, which is exactly the prediction problem that static features handle poorly in our experiments\.

## 3Integrating Learning Intogrind

grindruns an action loop, which can be viewed schematically as

solvers⊳instantiate⊳splitNext⊳mbtc\.\\texttt\{solvers\}\\;\\triangleright\\;\\texttt\{instantiate\}\\;\\triangleright\\;\\texttt\{splitNext\}\\;\\triangleright\\;\\texttt\{mbtc\}\.The loop repeats until it reaches a fixpoint or runs out of heartbeats\. On each pass, the subsolvers propagate known facts, instantiate lemmas, split goals, or close branches\.

We use three places where learned guidance can be inserted without forking the tactic: \(i\) thee\-matchinstance filter, which can discard low\-value instantiations before they enter the congruence structure; \(ii\) split\-target selection, implemented bysplitNext; and \(iii\) premise augmentation, which chooses facts to assert before the search begins\. Everything is Lean\-native with sub\-millisecond latency\. We summarize the data, features, and held\-out evaluation protocol in[AppendixA](https://arxiv.org/html/2607.22972#A1)\.

The learned components are deliberately small\. In this setting, where the model is applied matters more than how large it is, and our scaling results in[AppendixB](https://arxiv.org/html/2607.22972#A2)support this\. Thee\-matchfilter is a binary classifier that scores each candidate instantiation for proof\-relevance—whether it will appear in the final proof term\. It uses features of the lemma being instantiated, including its identity, head symbol, conclusion tokens, and premise tokens; matching features of the current goal; and a few numeric signals, such as thee\-matching round and how often the lemma has been useful before\. These form a135135\-dimensional vector fed to a three\-layer MLP \(135→64→32→1135\\\!\\to\\\!64\\\!\\to\\\!32\\\!\\to\\\!1\) trained with binary cross\-entropy\. The split\-study models are similarly small: MLPs and gradient\-boosted trees over goal\- and candidate\-level features \([AppendixC](https://arxiv.org/html/2607.22972#A3)\)\.

## 4Improvement 1: A Cost\-Awaree\-matchFilter

e\-matching\(Moura and Bjørner,[2007](https://arxiv.org/html/2607.22972#bib.bib3)\)instantiates quantified lemmas against the current e\-graph, which is maintained by congruence closure\(Nelson and Oppen,[1980](https://arxiv.org/html/2607.22972#bib.bib5)\)\. Many instantiations do not help the proof, but they still cost work–each match adds facts or terms that later solver components must maintain, and a single quantified lemma may match in many ways\.

We train a lightweight classifier on per\-instance features and use it at thee\-matchcall site to drop low\-value instantiations\. On a held\-out suite of855855theorems, the filter runs about5%5\\%faster, and additionally recovers\+2\+2solves over stockgrind\. Scaling training data by20×20\\timesdoes not broaden the niche, suggesting a limitation of the lemma\-identity mechanism rather than a shortage of examples\. We therefore treat the filter as a useful speed component and evidence for where static scoring is insufficient\.

## 5Improvement 2: Lookahead for Splitting

Whene\-matchand congruence closure stop making progress,grindfalls back on case splitting\. It chooses a fact and branches on its possible cases, for example,x=0x=0versusx≠0x\\neq 0, then continues the search separately on each branch\. The split target is chosen from a pool of candidates using a fixed numeric tie\-breaker\. A good split may close the goal quickly, while a bad split may create branches that grow until the tactic times out\.

To study this choice, we use an oracle experiment\. At each decision with multiple candidates, we force each candidate in turn, rerungrindwith the rest of the proof fixed, and record the outcome\. Each forced run is an actual execution of the policy that chooses that candidate\. In total, we collect about1616K forced\-choice outcomes from4,1204\{,\}120multi\-candidate decisions overnumina\.

### The main benefit addresses capability instead of speed\.

An oracle that always chooses the cheapest split reduces the total number of splits by only about4%4\\%\. The more interesting cases are failures of stockgrind\. In675675decisions,grind’s chosen split leads to a timeout\. In9797of those decisions \(14%14\\%\), at least one other split available at the same point closes the goal without new lemmas or extra search\. We call these the rescuable failures: they are the decisions where simply picking a different available candidate would have rescued the proof\.

For example, in a rational equation such as1/\(x\+1\)\+1/\(x\+2\)=1/x1/\(x\{\+\}1\)\+1/\(x\{\+\}2\)=1/x,grindmay split on a fact that sends one branch into a blow\-up and eventually times out\. A different available split would close the goal after a few more steps\. On these rescuable decisions, stockgrindhas a0%0\\%rescue rate by construction, while a uniformly random alternative succeeds57%57\\%of the time; see[Table1](https://arxiv.org/html/2607.22972#S5.T1)\. This leaves room for a better split policy\.

### Static prediction does not beat random on the rescuable failures\.

We tried four policies for choosing the rescuing split: a gradient\-boosted cost model\(Chen and Guestrin,[2016](https://arxiv.org/html/2607.22972#bib.bib20)\), a generation\-ordering rule validated on a held\-out cost metric, a doom/value model, and a failure\-aware success classifier with candidate AUC 0\.85 on by\-decision held\-out data\. None beats random on the rescuable decisions; see[Table1](https://arxiv.org/html/2607.22972#S5.T1)\. These models have strong aggregate metrics overall and presumably help on the easy or median decisions, but precisely on the decisions wheregrind’s own heuristic was wrong, the static models’ predictions are correlated enough withgrind’s signal that they tend to be wrong in the same way\. The missing information is whether a split will cause a branch to explode, which appears to be a dynamic property rather than one captured by our static features, outlined in[AppendixC](https://arxiv.org/html/2607.22972#A3)\.

Table 1:Static\-feature policies do not beat random on the rescuable split failures\. Lookahead succeeds because it tries the split instead of predicting its outcome from static features\.Policy \(on the rescuable split\-failures\)rescue rategrind\(stock heuristic\)0%GBM cost model / generation rule30–46%value\-doom / failure\-aware classifier46–53%uniform random57%*1\-step lookahead \(realized\)**100%*Lookahead captures most of the benefit by turning split selection into a small experiment\. For each candidate, the policy makes a throwaway copy of the goal, forces that split, and runsgrindon the copy for a bounded number of steps\. We say a trial closes when this bounded sub\-search proves the goal in the copy; the parent tactic commits to the first such candidate and discards the other copies\. Since the trial actually executes the split, it observes the dynamic behavior that the static models miss\. The question is therefore not whether lookahead can identify the rescuing split, but how much it costs to try\.

On the rescue decisions, a time\-capped trial recovers90%90\\%of rescuable failures with a1515s cap\. Even when every candidate is tried, the average trial cost remains below the timegrindwould otherwise spend following its bad choice to timeout \([Table2](https://arxiv.org/html/2607.22972#S5.T2)\)\.

Table 2:Time\-capped lookahead on the rescue decisions\. AtC=15C\{=\}15s it rescues90%90\\%of the rescuable failures, at lower cost than the approximately5353sgrindspends on its bad choice\.
### Proving theorems stockgrindmisses\.

We implemented the lookahead split policy insidegrind\. At each split, the tactic tries candidates on functionally discarded goal copies under an iteration budget, and commits to a candidate whose trial closes\.

We then ran the implementation live\. On the4444theorems whose traces contain a rescue decision, stockgrindsolves3939and times out on55under a deterministic400400K\-heartbeat budget\. Always\-on lookahead solves4242: it rescues all55stock failures, but regresses on22goals that stockgrindalready solves\. These regressions come from the greedy rule of taking the first candidate whose trial closes, which is not always globally best\.

This motivates the cascade deployment\. We first run stockgrind, and run lookahead only if stockgrindfails\. The3939stock solves are then left unchanged, so the22always\-on regressions do not occur, while the55stock failures are rescued\. On this set, the cascade solves44/4444/44theorems instead of39/4439/44, a net gain of55with no regressions, and uses fewer total splits \(10591059versus12711271at the 400K budget\)\.

### When lookahead works\.

Lookahead is a shallow probe: it rescues goals when the right split closes within the trial budget, but it is not a substitute for deeper search\. The55rescued theorems have shallow rescues: after the right split, the branch closes within roughly99further splits\. The22regressions require deeper, multi step commitments, with rescuing branches between1010and5757splits deep, sometimes spread across several sequential decisions\. In those cases, stockgrind’s ordinary unbounded search make the better long\-term choice\. Thus, the cascade is safer than enabling lookahead globally\.

Table 3:On rescuable decisions, dynamic execution is the lever\. A non\-learning probe that tries candidates in random order until one closes rescues nearly all of them \(≈\\approx96%96\\%, the remainder hitting the per\-decision trial cap\) in∼1\.6\{\\sim\}1\.6candidate trials on average, while the learned static policies of[Table1](https://arxiv.org/html/2607.22972#S5.T1)fall below even the random single pick\. “≤4\.6\\leq 4\.6trials” for the deployed lookahead is the average number of candidate trials it spends per rescue decision when run without ordering, bounded above by the per\-decision candidate count\. There is room for learning is in cost and reach \(when and how deep to probe\), not in naming the rescuing split\.

## 6Discussion: The Cascade Discipline

The trouble with putting a learned heuristic insidegrindis that the tactic’s search can blow up:e\-matching keeps generating new facts, so a choice that looks good at one step can leave the solver with far more work a few steps later\. A learned rule that is switched on all the time runs straight into this\. It steers some proofs to a quick close and sends others into blow\-up, and across a benchmark, the two can roughly cancel\.

Our fix is to never let the learned rule touch a proof that already works\. We run stockgrindfirst, and call the learned intervention only on the goals where stockgrindhas failed\. The lookahead applies this idea at a single split: try the alternatives, and keep one if it closes\. The filter is an easier version of it, dropping an instantiation only when it is confident the instantiation is useless\. The same recipe also helps with premise augmentation: if we add premises only as a retry aftergrindfails, we keep the rescues and lose nothing \([AppendixD](https://arxiv.org/html/2607.22972#A4)\)\.

This changes where we think learning should go\. It should be emphasized that the deployed split policy itself is non\-learned: it is a greedy first\-closing probe, and[Table3](https://arxiv.org/html/2607.22972#S5.T3)shows that a non\-learning random\-order bounded probe captures most of the benefit\. Learning is more suitable one layer up: deciding when lookahead is worth its cost, and which candidates to try first so the probe finds a closing trial in fewer attempts\.[Table1](https://arxiv.org/html/2607.22972#S5.T1)shows that a form of this, picking the right split from static features, does not work in the most impactful cases\. Four different models do about as well as random, likely because the most impactful features depends on what happens next, which the models struggle to learn\. What works is executing the split under a bounded budget and observing its behavior\. The job of a learned model is therefore not to name the split, but to help steer the search: a gating policy that decides when the probe is worth the time, and a candidate\-ordering policy that reduces the average probe cost\.

## 7Conclusion

We integrated learning into Lean 4’sgrindat several internal call sites and found two problem\-level improvements\. A cost\-awaree\-matchfilter gives a small success and speed improvement on a held\-out suite, while a bounded lookahead cascade proves five theorems stockgrindcannot, with zero regressions\. The results support a simple rule: preserve the symbolic solver as the default, and use learning to decide when and how to spend bounded search on the failures it leaves behind\.

Two directions follow directly from the analysis here\. First, the discussion identifies a concrete role for learning that we did not build: a gating model that decides when lookahead is worth running, and an ordering model that reduces the average candidate trials per rescue toward the perfect\-order baseline of 1\. Second, premise augmentation is a third natural intervention surface \([AppendixD](https://arxiv.org/html/2607.22972#A4)\); the patterns that protects the lookahead intervention from regression should extend to a learned premise retriever\.

## Impact Statement

This work studies machine\-learning interventions inside an automated reasoning tactic for the Lean 4 proof assistant\. The aim is to make formal verification more capable; we see no specific societal risks beyond those general to automated theorem proving\.

## Acknowledgements

We thank the UW Department of Applied Mathematics and the organizers of the University of Washington 2026 Lean Hackathon for access to compute\.

## References

- A\. A\. Alemi, F\. Chollet, N\. Een, G\. Irving, C\. Szegedy, and J\. Urban \(2016\)DeepMath – deep sequence models for premise selection\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- M\. Balunović, P\. Bielik, and M\. Vechev \(2018\)Learning to solve SMT formulas\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px1.p1.1)\.
- J\. C\. Blanchette, C\. Kaliszyk, L\. C\. Paulson, and J\. Urban \(2016\)Hammering towards QED\.Journal of Formalized Reasoning9\(1\),pp\. 101–148\.Cited by:[Appendix D](https://arxiv.org/html/2607.22972#A4.p1.2),[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- T\. Chen and C\. Guestrin \(2016\)XGBoost: a scalable tree boosting system\.InProceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining \(KDD\),pp\. 785–794\.Cited by:[§5](https://arxiv.org/html/2607.22972#S5.SS0.SSS0.Px2.p1.1)\.
- Ł\. Czajka and C\. Kaliszyk \(2018\)Hammer for Coq: automation for dependent type theory\.Journal of Automated Reasoning61\(1–4\),pp\. 423–453\.Cited by:[Appendix D](https://arxiv.org/html/2607.22972#A4.p1.2),[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- T\. Gauthier, C\. Kaliszyk, J\. Urban, R\. Kumar, and M\. Norrish \(2021\)TacticToe: learning to prove with tactics\.Journal of Automated Reasoning65\(2\),pp\. 257–286\.Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- V\. Kurin, S\. Godil, S\. Whiteson, and B\. Catanzaro \(2020\)Can Q\-learning with graph networks learn a generalizable branching heuristic for a SAT solver?\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px1.p1.1)\.
- G\. Lample, T\. Lacroix, M\. Lachaux, A\. Rodriguez, A\. Hayat, T\. Lavril, G\. Ebner, and X\. Martinet \(2022\)HyperTree proof search for neural theorem proving\.InAdvances in Neural Information Processing Systems \(NeurIPS\),Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- Lean FRO \(2024\)Thegrindtactic\.Note:The Lean Language Reference, chapter 16Accessed May 2026External Links:[Link](https://lean-lang.org/doc/reference/latest/The--grind--tactic/)Cited by:[§1](https://arxiv.org/html/2607.22972#S1.p2.1)\.
- L\. Moura and N\. Bjørner \(2007\)Efficient e\-matching for smt solvers\.InProceedings of the 21st International Conference on Automated Deduction \(CADE\-21\),Berlin, Heidelberg,pp\. 183–198\.External Links:ISBN 9783540735946,[Link](https://doi.org/10.1007/978-3-540-73595-3_13),[Document](https://dx.doi.org/10.1007/978-3-540-73595-3%5F13)Cited by:[§4](https://arxiv.org/html/2607.22972#S4.p1.1)\.
- L\. Moura and N\. Bjørner \(2008\)Z3: an efficient SMT solver\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS\),Lecture Notes in Computer Science, Vol\.4963,pp\. 337–340\.Cited by:[§1](https://arxiv.org/html/2607.22972#S1.p2.1)\.
- L\. Moura and S\. Ullrich \(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction \(CADE\-28\),Lecture Notes in Computer Science, Vol\.12699,pp\. 625–635\.Cited by:[§1](https://arxiv.org/html/2607.22972#S1.p2.1)\.
- G\. Nelson and D\. C\. Oppen \(1980\)Fast decision procedures based on congruence closure\.Journal of the ACM27\(2\),pp\. 356–364\.Cited by:[§4](https://arxiv.org/html/2607.22972#S4.p1.1)\.
- S\. Polu and I\. Sutskever \(2020\)Generative language modeling for automated theorem proving\.arXiv preprint arXiv:2009\.03393\.Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- S\. Ross, G\. J\. Gordon, and J\. A\. Bagnell \(2011\)A reduction of Imitation Learning and structured prediction to no\-regret online learning\.External Links:1011\.0686,[Link](https://arxiv.org/abs/1011.0686)Cited by:[Appendix C](https://arxiv.org/html/2607.22972#A3.p1.4)\.
- D\. Selsam, M\. Lamm, B\. Bünz, P\. Liang, L\. de Moura, and D\. L\. Dill \(2019\)Learning a SAT solver from single\-bit supervision\.InInternational Conference on Learning Representations \(ICLR\),Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px1.p1.1)\.
- D\. Silver, T\. Hubert, J\. Schrittwieser, I\. Antonoglou, M\. Lai, A\. Guez, M\. Lanctot, L\. Sifre, D\. Kumaran, T\. Graepel, T\. Lillicrap, K\. Simonyan, and D\. Hassabis \(2018\)A general reinforcement learning algorithm that masters chess, shogi, and Go through self\-play\.Science362\(6419\),pp\. 1140–1144\.Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.
- M\. Willsey, Y\. R\. Wang, O\. Flatt, C\. Nandi, P\. Panchekha, and Z\. Tatlock \(2020\)Egg: easy, efficient, and extensible e\-graphs\.CoRRabs/2004\.03082\.External Links:[Link](https://arxiv.org/abs/2004.03082),2004\.03082Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px2.p1.1)\.
- L\. Xu, F\. Hutter, H\. H\. Hoos, and K\. Leyton\-Brown \(2008\)SATzilla: portfolio\-based algorithm selection for SAT\.Journal of Artificial Intelligence Research \(JAIR\)32,pp\. 565–606\.Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px4.p1.1)\.
- K\. Yang, A\. Swope, A\. Gu, R\. Chalamala, P\. Song, S\. Yu, S\. Godil, R\. J\. Prenger, and A\. Anandkumar \(2023\)LeanDojo: theorem proving with retrieval\-augmented language models\.InAdvances in Neural Information Processing Systems \(NeurIPS\), Datasets and Benchmarks Track,Cited by:[§2](https://arxiv.org/html/2607.22972#S2.SS0.SSS0.Px3.p1.1)\.

## Appendix AModels, Data, and Held\-out Methodology

Held\-out invariant\.Two suites are held strictly out of all training: a7575\-theorem active\-split benchmark and an855855\-theorem held\-out suite \(held\_out\_v2\); a programmatic gate enforces that no training row originates from either\.Forced\-choice protocol\.For split analysis we instrument the trace observer to log, at each multi\-candidate decision, the candidategrindwould pick; we then re\-rungrindforcing each alternative candidate with the remainder of the proof fixed and record outcome and split count\. Because a forced run is a realized deployment of the policy that picks that candidate, the resulting rescue rates are measured, not projected\.Inference\.All learned scorers are exported to a native format read inside Lean, so scoring adds sub\-millisecond latency per decision\.

### Filter model and training\.

The filter is a concatenation MLP with no cross\-features\. Each instantiation is represented by eight1616\-dimensional embeddings—the lemma identity, its tokenized name, its head symbol, and pooled tokens of its conclusion and premises, together with the goal’s head symbol and pooled conclusion and premise tokens—plus seven numeric features \(thee\-matching round, the instance’s ordinal within the round, the number of new instances in the round, per\-theorem instance and round counts, and the lemma’s historical usefulness frequency and positive rate\)\. The resulting135135\-dimensional vector passes throughLinear​\(135,64\)→ReLU→Dropout​\(0\.1\)→Linear​\(64,32\)→ReLU→Linear​\(32,1\)\\mathrm\{Linear\}\(135,64\)\\\!\\to\\\!\\mathrm\{ReLU\}\\\!\\to\\\!\\mathrm\{Dropout\}\(0\.1\)\\\!\\to\\\!\\mathrm\{Linear\}\(64,32\)\\\!\\to\\\!\\mathrm\{ReLU\}\\\!\\to\\\!\\mathrm\{Linear\}\(32,1\), trained with binary cross\-entropy \(Adam\) to predict proof\-relevance: the label is11when the instance’s\(uid,lemma\)\(\\text\{uid\},\\text\{lemma\}\)pair appears in the closing proof term, recovered from aproof\_relevanttrace event\. The model is small by design—the shipped version trains on∼1\.2\{\\sim\}1\.2K Mathlib\-derived rows—and the scaling study \([AppendixB](https://arxiv.org/html/2607.22972#A2)\) confirms that capacity, not the architecture, is the limit\. At inference the weights are serialized to a fixed\-layout binary and scored by an evaluator compiled into the tactic, well under a millisecond per instance; an instance is dropped when its score falls below a thresholdτ\\tau, subject to a per\-round drop ratio\.

## Appendix BFilter: Negative and Niche Results

Data scaling plateaus\.Increasing augmented training rows by20×20\\times\(∼\\sim3\.9K to∼\\sim84K, sweeping the full eligiblefinelean\+numina\+workbookpool\) leaves held\-out success*exactly*at830/855830/855across configurations—zero marginal benefit, and−3\-3relative to our shipped Mathlib\-trained filter \(the833/855833/855of[Section4](https://arxiv.org/html/2607.22972#S4); stockgrindsolves831831\)\.Lemma vocabulary is not the bottleneck\.Inline trace\-time feature capture grows the lemma vocabulary3\.5×3\.5\\times\(73→25773\\to 257\) and lifts test AUC0\.949→0\.9550\.949\\to 0\.955, but held\-out gains only\+1\+1\(829→830829\\to 830\)\.Threshold tuning does not bridge the gap\.Sweeping\(τ,drop\_ratio\)\(\\tau,\\text\{drop\\\_ratio\}\)over five settings holds success flat at829829–830830; none reaches the shipped filter’s833833\.Balancing helps once, then hurts\.A balanced≈32/32/2/34%\\approx\\\!32/32/2/34\\%mix scores832832with fewer rows, but doubling the data while up\-weighting one source \(14×14\\timesmoreworkbook\) regresses to829829: distribution balancing is necessary but not sufficient; label quality differs across sources\.Pipeline is faithful\.Re\-running the shipped filter’s exact Mathlib dataset through the new pipeline reproduces833/855833/855, so the deficit is data composition, not a pipeline regression\.

Where the\+2\+2lives\.A per\-bucket breakdown shows the filter is a near\-exact no\-op on the easy/medium≈79%\\approx\\\!79\\%of the benchmark; all movement is in the hard bucket\. The\+2\+2are three near\-duplicate square\-root recurrence theorems minus one loss\. A controlled synthetic sweep of120120leak\-free integer recurrences finds the filter exactly inert \(0rescued,0broken\): scoring by*lemma identity*, it cannot distinguish wasteful from useful instances of the*same*hypothesis, so it helps only when the explosion is lemma\-*diverse*\. On the low\-contention partition, paired repeated trials give the filter−4\.9%\-4\.9\\%walltime \(95% CI\[−20\.3,−16\.0\]\[\-20\.3,\-16\.0\]s\) while solving\+2\+2every repetition\.

## Appendix CSplit: Static\-Model Details

The four static\-feature policies behind[Table1](https://arxiv.org/html/2607.22972#S5.T1)are: a gradient\-boosted cost regressor; a generation\-ordering rule \(validated held\-out at\+9\.5\+9\.5points optimal\-pick on a cost metric\); a doom/value model trained on all rollouts in a DAgger\-style loop\(Rosset al\.,[2011](https://arxiv.org/html/2607.22972#bib.bib14)\)\(success\-prediction AUC0\.9840\.984at the state level\); and a failure\-aware success classifier trained on∼15\{\\sim\}15K forced\-choice labels with candidate\-level AUC0\.850\.85, all evaluated by\-decision held\-out\. They score the same goal\- and candidate\-level features: the number of cases a split induces, whether it is recursive, the source theory, the generation depth, the split depth, and the number ofe\-matching rounds so far\. Despite strong aggregate metrics, every one is at or below uniform random on the rescuable split\-failures, because the discriminative signal \(whether a split explodes\) is dynamic and not present in the static features\.

### Per\-theorem behavior\.

[Table4](https://arxiv.org/html/2607.22972#A3.T4)lists the seven decisivenuminacases behind the live cascade result of[Section5](https://arxiv.org/html/2607.22972#S5): the fivegrindtimeouts the cascade rescues, and the two goals where always\-on lookahead regresses but the cascade does not \(it never runs lookahead on a goal stock already solves\)\. Rescue depth is the minimum number of further splits the rescuing branch needs to close\.

theoremstocklookaheadcascaderescue depth000125timeoutsolvesolve9000281timeoutsolvesolve9000470timeoutsolvesolve5000530timeoutsolvesolve4000619timeoutsolvesolve3000027solvetimeoutsolve57000220solvetimeoutsolve10Table 4:Per\-theorem behavior on the seven decisive cases \(anonymizednuminaIDs\)\. Top: the five stock timeouts the cascade rescues\. Bottom: the two goals where always\-on lookahead regresses, which the cascade leaves to stock and therefore still solves\.

## Appendix DPremise Augmentation

Table 5:Premise\-augmentation oracle onnumina\. Even ground\-truth premises rescue∼2%\{\\sim\}2\\%of failures but break∼1/4\{\\sim\}1/4of the \(few\) solves viae\-matchblowup, netting≈0\{\\approx\}0\.The additive lever is small and idea\-gap\-bound: most failures lack a proof*idea*\(intermediate steps, constructions\), not a citable lemma—the “idea gap” familiar from hammer evaluations\(Blanchetteet al\.,[2016](https://arxiv.org/html/2607.22972#bib.bib12); Czajka and Kaliszyk,[2018](https://arxiv.org/html/2607.22972#bib.bib13)\)—and the premises that are added themselves triggere\-matchblowup\. But a failure\-triggered cascade \(run plaingrind; only on failure retry with premises\) banks the rescues with zero regression by construction\. Of the rescues,≈53%\{\\approx\}53\\%need a single premise and≈74%\{\\approx\}74\\%need at most two, favoring retrieval over a fixed\-vocabulary classifier\.