REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Published in arXiv, 2025
Recommended citation: Shen, Z., Huang, N., Yang, F., Wang, Y., Gao, G., Xu, T., Jiang, J., He, W., Yang, P., Sun, M., Ju, H., Wu, P., Dai, B., & Dong, B. (2025). REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning. arXiv preprint arXiv:2505.20613. https://arxiv.org/abs/2505.20613
Formal theorem provers have made rapid progress on competition-level mathematics, but generalization to advanced mathematics remains difficult. REAL-Prover is a retrieval-augmented Lean 4 theorem prover that combines a fine-tuned large language model, a retrieval system, and new data-generation tools to improve college-level mathematical reasoning.