REAL-Prover: Retrieval Augmented Lean Prover

REAL-Prover, developed by FrenzyMath, is a 7.6 billion parameter language model specifically engineered for formal mathematical reasoning within the Lean 4 theorem prover. Built on Qwen2.5-Math-7B, it integrates a novel retrieval-augmented generation pipeline to enhance its proof-generating capabilities.

Key Capabilities

• Retrieval-Augmented Reasoning: Utilizes a retrieval module, Leansearch-PS, to dynamically fetch relevant theorems from the Lean math library, significantly improving the quality and accuracy of generated proofs.
• Stepwise Theorem Proving: Designed to generate proofs in a step-by-step manner, making the reasoning process more transparent and verifiable.
• Custom Training: Fine-tuned using a specialized pipeline and dataset, including data synthesized in an interactive environment (Jixia-interactive).
• Comprehensive Evaluation: Assessed on established benchmarks like ProofNet and a newly proposed benchmark, FATE-M, to validate its performance in formal mathematics.

Good for

• Automated Theorem Proving in Lean 4: Ideal for researchers and developers working on automating proof generation within the Lean 4 ecosystem.
• Mathematical Research: Supports advanced mathematical reasoning tasks requiring formal verification.
• Developing AI for Formal Systems: Provides a robust foundation for exploring retrieval-augmented approaches in symbolic AI and formal methods.