PaperlayerView exact revision on arXiv

Source-linked AI summary

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai, Bin Dong

arXiv:2505.20613v3cs.CLcs.AIcs.LGcs.LO

TL;DR

Advanced mathematics remains difficult for formal theorem provers because of data sparsity, domain-specific reasoning, and precise use of extensive lemma libraries. REAL-Prover combines stepwise Lean proving with theorem retrieval and reports strong results on college-level benchmarks, including a state-of-the-art result on FATE-M.

  • Problem

    Formal theorem provers still struggle to generalize to undergraduate and graduate mathematics amid data sparsity, domain-specific reasoning, and the need to use extensive lemma libraries precisely.

    Source: §1 · p. 3

  • Method

    REAL-Prover is a stepwise Lean framework that conditions each invocation on the current proof state and retrieves relevant Mathlib theorems, supported by HERALD-AF, Jixia-Interactive, and expert iteration.

    Source: §1 · p. 3, §1.2 · p. 4, §2.2 · p. 6

  • Results

    REAL-Prover achieved a 23.7% success rate on ProofNet and a 56.7% Pass@64 on FATE-M, reported as state of the art.

    Source: §4.1 · p. 10, §4.2 · p. 10

  • Takeaways & Limitations

    On ProofNet and FATE-M, the same-data model with retrieval outperformed its no-retrieval counterpart.

    Source: §4.4 · p. 12

    The model uses supervised objectives without reinforcement learning, which the authors have not incorporated because of computational demands.

    Source: §5 · p. 13

Abstract

from arXiv · show

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).

1 Introduction

REAL-Prover targets the challenge of extending automated theorem proving beyond high-school mathematics, combining stepwise Lean proof generation with retrieval and new data and benchmark resources. The paper reports strong results on its graduate-level algebra benchmark and competitive performance on existing benchmarks.

1 Introduction

  • Advanced mathematics remains challenging for automated provers because of sparse data, domain-specific reasoning, and the need to retrieve and apply extensive lemma libraries precisely.The passage notes that minor inaccuracies can compromise purely neural proof generation.Source: §1 · p. 3
  • 56.7% accuracy on FATE-M is reported for REAL-Prover, which also demonstrates competitive performance on miniF2F and ProofNet.The paper presents FATE-M as a benchmark for graduate-level reasoning in algebraic domains.Source: §1 · p. 3

1.1 Related works

  • Whole-proof approaches can struggle with error accumulation and implicit state inference, while interactive proof-step systems use prover feedback to guide tactic generation and search.Existing benchmarks include Olympiad-level miniF2F and undergraduate-level ProofNet, motivating more challenging graduate-level tests.Source: §1.1 · pp. 3–4

1.2 Our Contributions

  • REAL-Prover integrates informal-to-formal data generation, retrieval-augmented stepwise proving, and a Lean 4 interactive environment for graduate-level formal mathematics.The system includes HERALD-AF, LeanSearch-PS, and Jixia-Interactive.Source: §1.2 · p. 4
  • The released dataset contains 55k state–tactic pairs, each pairing a formal proof state and context with a corresponding tactic sequence.The pairs are generated through expert iteration and intended to supervise proof-search optimization and policy learning.Source: §1.2 · p. 4
  • FATE-M provides paired informal-formal problems in graduate-level abstract algebra, complementing miniF2F and ProofNet for formal-reasoning evaluation.Its scope includes abstract algebra rather than only Olympiad-level or undergraduate-level problems.Source: §1.2 · p. 4

2 Method

The method builds a loop from informal mathematical statements to formal Lean statements and then verified proofs. REAL-Prover explores proof states with best-first search, retrieval-conditioned tactics, and iterative training-data collection.

2.1 HERALD-AF

  • HERALD-AF generates candidate Lean statements, translates them back into natural language, and retains only statements judged faithful to the original input.The pipeline first extracts and refines informal statements from a natural-language mathematics corpus.Source: §2.1 · p. 5

2.2 REAL-Prover

  • REAL-Prover builds a search tree by applying candidate tactics through Jixia-interactive, which updates proof states and discards invalid tactics.The process continues until proof completion or the search budget is exhausted, after which the proof can be reconstructed from the tree.Source: §2.2 · pp. 5–6
  • The prover uses best-first search, expanding the highest-scoring proof state and conditioning tactic generation on retrieved Mathlib information.The loop ends when a proof is completed or the predefined search budget runs out.Source: §2.2 · p. 6, Figure 2 · p. 6

2.2.1 LeanSearch-PS

  • LeanSearch-PS embeds proof states and Mathlib theorems in a shared semantic space, retrieves top-k theorems, and supplies them as context to the language model.Its embedding model uses proof-state/theorem pairs and a two-stage training process, including mined hard negatives.Source: §2.2.1 · pp. 6–7

2.2.2 Expert Iteration

  • Expert iteration uses the prover to solve HERALD-AF statements, adds successful generated data to supervised fine-tuning, and repeats with the improved model.The refined model is then applied to challenging statements the previous model could not solve.Source: §2.2.2 · p. 7

3 Experiment Setup

REAL-Prover is trained on state-tactic examples and uses LeanSearch-PS retrieval during proof generation. The experiments evaluate it on algebra-focused FATE-M and the broader ProofNet and MiniF2F benchmarks.

3.1 Implementation Detail

  • REAL-Prover-v1 is supervised-fine-tuned from Qwen2.5-Math-7B on 210,420 state-tactic pairs drawn from expert-iteration proofs, human annotations, Mathlib, and Lean-Workbook.The expert-iteration material includes algebra and NuminaMath problems, while the human-annotated set is based on 196 undergraduate algebra problems.Source: §3.1 · pp. 7–8
  • LeanSearch-PS uses two-stage dense-retriever training with hard negatives, while inference uses 64 passes and samples per step, temperature 1.5, and score parameter α=0.5.Hard negatives are randomly selected from each query’s top-30-to-top-100 most similar theorem passages.Source: §3.1 · p. 8

3.2 Benchmark

  • The evaluation also uses ProofNet for undergraduate mathematics and MiniF2F for Olympiad-level problems, following prior work to assess general capabilities.ProofNet has 185 validation and 186 test problems; MiniF2F has 244 validation and 244 test problems.Source: §3.2 · p. 9
  • FATE-M contains 141 Lean4-formalized undergraduate abstract algebra problems, with statements checked by Mathlib contributors and algebra PhD students and Lean-checked proofs supplied.The problems were extracted from 12 university-level abstract algebra textbooks and formalized by students.Source: §3.2 · p. 9

4 Quantitative Result

The section reports REAL-Prover results on college-level ProofNet and FATE-M, tests generalization on MiniF2F, and examines the effect of retrieval.

4.1 ProofNet Result

  • 23.7% success rate on ProofNet with retrieval and supervised fine-tuning alone surpassed two reinforcement-learning systems at the stated sampling budgets.The comparison is with DeepSeek-Prover-V1.5-RL under a 3200-sampling budget and DeepSeek-Prover-V1.5-RL+RMaxTS under 1×3200 sampling.Source: §4.1 · p. 10, Table 1 · p. 11

4.2 FATE-M Result

  • 56.7% Pass@64 on FATE-M was a state-of-the-art result among the evaluated systems.The benchmark evaluates college-level algebraic problems.Source: §4.2 · p. 10, Table 2 · p. 11

4.3 MiniF2F Result

  • REAL-Prover performed relatively poorly against state-of-the-art systems on MiniF2F.The authors suggest retrieval helps less on its high-school olympiad problems, which often do not rely heavily on Mathlib, and note their model used supervised fine-tuning without reinforcement learning.Source: §4.3 · p. 11, Table 3 · p. 12

4.4 Ablation Study

  • With the same dataset, REAL-Prover-v1 outperformed its version without retrieval on both ProofNet and FATE-M.The ablation compares REAL-Prover-v1 with LeanSearch-PS enabled against REAL-Prover-v1-NoRet without it.Source: §4.4 · p. 12, Table 4 · p. 12
  • In the illustrated case, LeanSearch-PS retrieved critical lemmas and completed verification, while the proof without retrieval failed verification.For problems solvable with either setup, the authors report that retrieval often yields more accurate and human-readable proofs.Source: §4.4 · p. 13, Figure 3 · p. 13

5 Conclusion and Future Work

REAL-Prover combines stepwise Lean 4 proof generation with HERALD-AF, Jixia-Interactive, and LeanSearch-PS, and the paper reports a state-of-the-art 56.7% success rate on FATE-M. The authors identify supervised-only training and tactic-only outputs as current limitations, with RL fine-tuning and informal reasoning proposed as future directions.

5 Conclusion and Future Work

  • 56.7% success rate on FATE-M is reported as state of the art for REAL-Prover.The benchmark focuses on algebraic problems.Source: §5 · p. 13
  • REAL-Prover is a stepwise Lean 4 prover supported by HERALD-AF, Jixia-Interactive, and LeanSearch-PS.HERALD-AF translates informal mathematical statements into formal representations, while Jixia-Interactive supports training and proof generation.Source: §5 · p. 13
  • The current model uses supervised objectives only, and REAL-Prover emits final Lean tactics without a natural-language chain-of-thought stage.The authors say RL has not been incorporated due to computational demands.Source: §5 · p. 13
  • Future work proposes RL-based fine-tuning and CoT-driven informal reasoning, with expected gains in reasoning, generalization, autonomy, interpretability, and robustness.The informal-reasoning layer is proposed to draft, filter, and organize candidate arguments before formal tactics.Source: §5 · p. 14

A Prompt for REAL-Prover

The prompt example presents Lean proof construction as iterative tactic application, with the current proof state recording the remaining goals and local context. Its sample asks for a tactic to solve a state and supplies potentially helpful theorem statements.

A Prompt for REAL-Prover

  • A Lean proof is a complete proof term checked by the kernel, while a tactic-based state records remaining goals and local context.The prompt example shows a state with hypotheses and an unsolved goal.Source: A Prompt for REAL-Prover · p. 19
  • Tactics incrementally transform proof states, and once all goals are solved, Lean assembles and kernel-checks the resulting proof term.The state after a tactic reflects the goals that remain.Source: A Prompt for REAL-Prover · p. 19
  • The example prompt asks for a Lean 4 tactic for the current state and supplies theorem statements as potentially helpful references.The displayed state includes hypotheses h1 and h2 and a goal about real parts of complex numbers.Source: A Prompt for REAL-Prover · p. 19

B Source Textbooks for FATE-M

FATE-M draws problems from a set of abstract algebra textbooks, including the titles listed below.

B Source Textbooks for FATE-M

  • The listed sources include Pinter’s A Book of Abstract Algebra, Fraleigh’s A First Course in Abstract Algebra, Anderson and Feil’s A First Course in Abstract Algebra: Rings, Groups, and Fields, and Rotman’s A First Course in Abstract Algebra with Applications.Source: B Source Textbooks for FATE-M · p. 20
  • Other listed sources are Hodge, Schlicker, and Sundstrom’s Abstract Algebra: An Inquiry-Based Approach, Herstein’s Abstract Algebra, Grillet’s Abstract Algebra, and Choudhary’s Abstract Algebra.Source: B Source Textbooks for FATE-M · p. 20
  • The source list also includes Saracino’s Abstract Algebra: A First Course, Hungerford’s Abstract Algebra: An Introduction, Dummit and Foote’s Abstract Algebra, and Feng and Zhang’s 300 Problems in Abstract Algebra.Source: B Source Textbooks for FATE-M · p. 20

C Training Details

REAL-Prover training and LeanSearch-PS training use separate GPU setups and runtimes, with their hyperparameters reported in separate tables.

C Training Details

D Broader Impacts

The authors describe possible benefits for proof construction, education, and mathematical discovery, while warning about opacity, educational overreliance, and reward hacking.

D Broader Impacts

  • Automated formal proofs may assist mathematicians, support proof-assistant teaching, and potentially contribute to conjecture exploration or novel proofs.The paper lists these as potential positive impacts.Source: D Broader Impacts · p. 21
  • Generated proofs may be opaque, excessive reliance may hinder mathematical understanding, and training may yield formally valid but semantically misleading proofs.The authors note reward hacking risks in the complex, nondeterministic Lean environment.Source: D Broader Impacts · p. 21
  • The authors call for careful evaluation, interpretability mechanisms, and human-in-the-loop verification for responsible use.Source: D Broader Impacts · p. 21

E Case study

Two FATE-M examples show valid proofs with and without LeanSearch-PS, while proofs using premise selection are described as often faster and more readable.

E Case study

  • Both REAL-Prover-v1 variants produce valid results, while the LeanSearch-PS version often produces faster and more readable proofs.The paper presents two FATE-M cases illustrating this comparison in Figures 4 and 5.Source: E Case study · p. 21, Figure 4 · p. 22, Figure 5 · p. 22
  • Figure 4’s proof with LeanSearch-PS uses Mathlib’s existing IsAlgClosed.instInfinite instance and is described as more readable.Source: Figure 4 · p. 22
  • Figure 5’s proof with LeanSearch-PS uses Mathlib’s existing IsPGroup.of_surjective instance and is described as more readable.Source: Figure 5 · p. 22
Loading 2505.20613v3…