# HyperTree Proof Search for Neural Theorem Proving

arXiv: https://arxiv.org/abs/2205.11491 · HTML: https://mlsanity.com/paper/2205.11491/

## Key facts

- Cited by 197 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 69 references that are in the map.
- First posted on arXiv 23 May 2022.

## Builds on (most cited first, 30 of 30)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [Neural Machine Translation of Rare Words with Subword Units](https://mlsanity.com/paper/1508.07909/) (2015)
- [Cross-lingual Language Model Pretraining](https://mlsanity.com/paper/1901.07291/) (2019)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Reducing Transformer Depth on Demand with Structured Dropout](https://mlsanity.com/paper/1909.11556/) (2019)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [MASS: Masked Sequence to Sequence Pre-training for Language Generation](https://mlsanity.com/paper/1905.02450/) (2019)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients](https://mlsanity.com/paper/1912.04871/) (2019)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Unsupervised Translation of Programming Languages](https://mlsanity.com/paper/2006.03511/) (2020)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Deep Encoder, Shallow Decoder: Reevaluating Non-autoregressive Machine Translation](https://mlsanity.com/paper/2006.10369/) (2020)
- [Massively Parallel Methods for Deep Reinforcement Learning](https://mlsanity.com/paper/1507.04296/) (2015)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Monte-Carlo Tree Search as Regularized Policy Optimization](https://mlsanity.com/paper/2007.12509/) (2020)
- [Deep Symbolic Regression for Recurrent Sequences](https://mlsanity.com/paper/2201.04600/) (2022)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)

## Built on by (most cited first, 30 of 197)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Augmented Language Models: a Survey](https://mlsanity.com/paper/2302.07842/) (2023)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Tool Learning with Foundation Models](https://mlsanity.com/paper/2304.08354/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [The Alignment Problem from a Deep Learning Perspective](https://mlsanity.com/paper/2209.00626/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Mulberry: Empowering MLLM with o1-like Reasoning and Reflection via Collective Monte Carlo Tree Search](https://mlsanity.com/paper/2412.18319/) (2024)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Progressive-Hint Prompting Improves Reasoning in Large Language Models](https://mlsanity.com/paper/2304.09797/) (2023)
- [From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models](https://mlsanity.com/paper/2406.16838/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning](https://mlsanity.com/paper/2402.06332/) (2024)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening](https://mlsanity.com/paper/2506.02355/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Efficient Test-Time Scaling via Self-Calibration](https://mlsanity.com/paper/2503.00031/) (2025)
- [Lean-STaR: Learning to Interleave Thinking and Proving](https://mlsanity.com/paper/2407.10040/) (2024)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Aristotle: IMO-level Automated Theorem Proving](https://mlsanity.com/paper/2510.01346/) (2025)

## Abstract (arXiv)

We propose an online training procedure for a transformer-based automated theorem prover. Our approach leverages a new search algorithm, HyperTree Proof Search (HTPS), inspired by the recent success of AlphaZero. Our model learns from previous proof searches through online training, allowing it to generalize to domains far from the training distribution. We report detailed ablations of our pipeline's main components by studying performance on three environments of increasing complexity. In particular, we show that with HTPS alone, a model trained on annotated proofs manages to prove 65.4% of a held-out set of Metamath theorems, significantly outperforming the previous state of the art of 56.5% by GPT-f. Online training on these unproved theorems increases accuracy to 82.6%. With a similar computational budget, we improve the state of the art on the Lean-based miniF2F-curriculum dataset from 31% to 42% proving accuracy.