# REFACTOR: Learning to Extract Theorems from Proofs

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

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 28 of its 48 references that are in the map.
- First posted on arXiv 26 Feb 2024.

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

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Fast Graph Representation Learning with PyTorch Geometric](https://mlsanity.com/paper/1903.02428/) (2019)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Neural Module Networks](https://mlsanity.com/paper/1511.02799/) (2015)
- [The Neuro-Symbolic Concept Learner: Interpreting Scenes, Words, and Sentences From Natural Supervision](https://mlsanity.com/paper/1904.12584/) (2019)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Compositional Attention Networks for Machine Reasoning](https://mlsanity.com/paper/1803.03067/) (2018)
- [DreamCoder: Growing generalizable, interpretable knowledge with wake-sleep Bayesian program learning](https://mlsanity.com/paper/2006.08381/) (2020)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [A Neuro-vector-symbolic Architecture for Solving Raven's Progressive Matrices](https://mlsanity.com/paper/2203.04571/) (2022)
- [Top-Down Synthesis for Library Learning](https://mlsanity.com/paper/2211.16605/) (2022)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [The Scattering Compositional Learner: Discovering Objects, Attributes, Relationships in Analogical Reasoning](https://mlsanity.com/paper/2007.04212/) (2020)
- [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)
- [Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar](https://mlsanity.com/paper/1912.02636/) (2019)
- [Automatically Composing Representation Transformations as a Means for Generalization](https://mlsanity.com/paper/1807.04640/) (2018)
- [Differentiable Programs with Neural Libraries](https://mlsanity.com/paper/1611.02109/) (2016)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Guiding Inferences in Connection Tableau by Recurrent Neural Networks](https://mlsanity.com/paper/1905.07961/) (2019)
- [Learning-assisted Theorem Proving with Millions of Lemmas](https://mlsanity.com/paper/1402.3578/) (2014)
- [Sharing HOL4 and HOL Light proof knowledge](https://mlsanity.com/paper/1509.03527/) (2015)
- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)

## Built on by (most cited first, 9 of 9)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Varying Shades of Wrong: Aligning LLMs with Wrong Answers Only](https://mlsanity.com/paper/2410.11055/) (2024)
- [Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Proving](https://mlsanity.com/paper/2506.17104/) (2025)
- [Action abstractions for amortized sampling](https://mlsanity.com/paper/2410.15184/) (2024)
- [Library Learning Doesn't: The Curious Case of the Single-Use "Library"](https://mlsanity.com/paper/2410.20274/) (2024)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [A Compute-Matched Re-Evaluation of TroVE on MATH](https://mlsanity.com/paper/2507.22069/) (2025)
- [Mathematical Derivation Graphs: A Relation Extraction Task in STEM Manuscripts](https://mlsanity.com/paper/2410.21324/) (2024)

## Abstract (arXiv)

Human mathematicians are often good at recognizing modular and reusable theorems that make complex mathematical results within reach. In this paper, we propose a novel method called theoREm-from-prooF extrACTOR (REFACTOR) for training neural networks to mimic this ability in formal mathematical theorem proving. We show on a set of unseen proofs, REFACTOR is able to extract 19.6% of the theorems that humans would use to write the proofs. When applying the model to the existing Metamath library, REFACTOR extracted 16 new theorems. With newly extracted theorems, we show that the existing proofs in the MetaMath database can be refactored. The new theorems are used very frequently after refactoring, with an average usage of 733.5 times, and help shorten the proof lengths. Lastly, we demonstrate that the prover trained on the new-theorem refactored dataset proves more test theorems and outperforms state-of-the-art baselines by frequently leveraging a diverse set of newly extracted theorems. Code can be found at https://github.com/jinpz/refactor.