REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning

arXiv REAL-Prover License: Apache 2.0 Lean 4

1. Overview

REAL-Prover is a retrieval-augmented, stepwise large language model-based theorem prover for Lean 4. It is built on top of Qwen2.5-Math-7B, and fine-tuned using our custom pipeline and dataset to support formal reasoning in Lean. The model is integrated with a retrieval module (Leansearch-PS) that fetches relevant theorems from the Lean math library to enhance generation quality.

Our approach introduces several innovations:

  • A retrieval-enhanced generation pipeline
  • A custom interactive environment (Jixia-interactive) for data synthesis
  • Evaluations on both ProofNet and our proposed benchmark FATE-M

2. Associated Paper

REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
arXiv:2505.20613

3. Running Experiments

Repository: https://github.com/frenzymath/REAL-Prover

Input Data Format

Each input data should be a JSONL line with two keys: id and formal_statement. See data/minif2f_test.jsonl for examples.

Running

Create a runtime configuration file (in TOML format) in ./experiment/examples/, then run:

cd Realprover
python -m experiment.run /path/to/config.toml

4. Citation

@misc{realprover2025,
      title={REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning}, 
      author={Ziju Shen and Naohao Huang and Fanyi Yang and Yutong Wang and Guoxiong Gao and Tianyi Xu and Jiedong Jiang and Wanyi He and Pu Yang and Mengzhou Sun and Haocheng Ju and Peihao Wu and Bryan Dai and Bin Dong},
      year={2025},
      eprint={2505.20613},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2505.20613}, 
}
Downloads last month
1
Safetensors
Model size
7.62B params
Tensor type
BF16
ยท
Inference Providers NEW
This model isn't deployed by any Inference Provider. ๐Ÿ™‹ Ask for provider support

Model tree for FrenzyMath/REAL-Prover

Base model

Qwen/Qwen2.5-7B
Finetuned
(401)
this model