# Towards Finding Longer Proofs

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 May 2019.

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Simplifying Polylogarithms with Machine Learning](https://mlsanity.com/paper/2206.04115/) (2022)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Project proposal: A modular reinforcement learning based automated theorem prover](https://mlsanity.com/paper/2209.02562/) (2022)
- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)
- [Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models](https://mlsanity.com/paper/2506.08171/) (2025)
- [Partial Label Learning for Automated Theorem Proving](https://mlsanity.com/paper/2507.03314/) (2025)

## Abstract (arXiv)

We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we focus on generalising from very little training data and achieving near complete confidence. We use several simple, structured datasets with very long proofs to show that FLoP can successfully generalise a single training proof to a large class of related problems. On these benchmarks, FLoP is competitive with strong theorem provers despite using very limited search, due to its ability to solve problems that are prohibitively long for other systems.