# Towards Finding Longer Proofs

## TL;DR

This paper introduces a reinforcement learning guidance system for automated theorem proving that effectively generalizes from minimal data to find longer proofs, outperforming traditional methods on complex benchmarks.

## Contribution

The work presents a novel RL-based approach that generalizes from limited training data to produce longer proofs, demonstrating competitive performance on challenging datasets.

## Key findings

- FLoP successfully generalizes from a single proof to related problems.
- FLoP can find longer proofs than existing systems on benchmark datasets.
- The approach requires limited search due to its effective guidance.

## Abstract

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.