# Learning Equational Theorem Proving

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Placed in Imitation learning methods, one of 13 directions in Offline RL and imitation learning from data.
- Builds on 14 of its 44 references that are in the map.
- First posted on arXiv 10 Feb 2021.

## Placed in

- Offline RL and imitation learning from data / [Imitation learning methods](https://mlsanity.com/offlinerl/imitation-learning-methods/)

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

- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Asynchronous Methods for Deep Reinforcement Learning](https://mlsanity.com/paper/1602.01783/) (2016)
- [Dota 2 with Large Scale Deep Reinforcement Learning](https://mlsanity.com/paper/1912.06680/) (2019)
- [Behavioral Cloning from Observation](https://mlsanity.com/paper/1805.01954/) (2018)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Sample Efficient Actor-Critic with Experience Replay](https://mlsanity.com/paper/1611.01224/) (2016)
- [Self-Imitation Learning](https://mlsanity.com/paper/1806.05635/) (2018)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [Can Neural Networks Learn Symbolic Rewriting?](https://mlsanity.com/paper/1911.04873/) (2019)
- [Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic](https://mlsanity.com/paper/1910.11797/) (2019)
- [Tree Neural Networks in HOL4](https://mlsanity.com/paper/2009.01827/) (2020)

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Similarity-Based Equational Inference in Physics](https://mlsanity.com/paper/2103.13496/) (2021)
- [PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physics](https://mlsanity.com/paper/2201.04275/) (2022)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)

## Abstract (arXiv)

We develop Stratified Shortest Solution Imitation Learning (3SIL) to learn equational theorem proving in a deep reinforcement learning (RL) setting. The self-trained models achieve state-of-the-art performance in proving problems generated by one of the top open conjectures in quasigroup theory, the Abelian Inner Mapping (AIM) Conjecture. To develop the methods, we first use two simpler arithmetic rewriting tasks that share tree-structured proof states and sparse rewards with the AIM problems. On these tasks, 3SIL is shown to significantly outperform several established RL and imitation learning methods. The final system is then evaluated in a standalone and cooperative mode on the AIM problems. The standalone 3SIL-trained system proves in 60 seconds more theorems (70.2%) than the complex, hand-engineered Waldmeister system (65.5%). In the cooperative mode, the final system is combined with the Prover9 system, proving in 2 seconds what standalone Prover9 proves in 60 seconds.