REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

TL;DR

REAL-Prover is an open-source, retrieval-augmented theorem prover for Lean 4 that significantly advances the automation of college-level mathematics by integrating large language models and retrieval systems.

Contribution

The paper introduces REAL-Prover, a novel retrieval-augmented theorem prover for Lean 4, with a new data pipeline and benchmark, achieving state-of-the-art results on algebraic problems.

Findings

Achieves 23.7% success rate on ProofNet dataset.

Attains 56.7% success rate on FATE-M benchmark.

Demonstrates the effectiveness of retrieval-augmented reasoning in formal theorem proving.

Abstract

Nowadays, formal theorem provers have made monumental progress on high-school and competition-level mathematics, but few of them generalize to more advanced mathematics. In this paper, we present REAL-Prover, a new open-source stepwise theorem prover for Lean 4 to push this boundary. This prover, based on our fine-tuned large language model (REAL-Prover-v1) and integrated with a retrieval system (Leansearch-PS), notably boosts performance on solving college-level mathematics problems. To train REAL-Prover-v1, we developed HERALD-AF, a data extraction pipeline that converts natural language math problems into formal statements, and a new open-source Lean 4 interactive environment (Jixia-interactive) to facilitate synthesis data collection. In our experiments, our prover using only supervised fine-tune achieves competitive results with a 23.7% success rate (Pass@64) on the ProofNet dataset-comparable to state-of-the-art (SOTA) models. To further evaluate our approach, we introduce FATE-M, a new benchmark focused on algebraic problems, where our prover achieves a SOTA success rate of 56.7% (Pass@64).