Update README.md

README.md

@@ -1,3 +1,77 @@
----
-license: apache-2.0
----
+---
+license: apache-2.0
+datasets:
+- your-org/expr_2000
+language:
+- en
+base_model:
+- Qwen/Qwen2.5-Math-7B
+pipeline_tag: text-generation
+library_name: transformers
+tags:
+- lean4
+- theorem-proving
+- formal-mathematics
+- retrieval-augmented
+- mathematical-reasoning
+---
+
+<div align="center">
+  <h1 style="font-size: 2.0em;">REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning</h1>
+  <div style="display: flex; justify-content: center; gap: 8px; flex-wrap: wrap;">
+    <a href="https://arxiv.org/abs/2505.20613"><img src="https://img.shields.io/badge/arXiv-Paper-b31b1b.svg" alt="arXiv"></a>
+    <a href="https://github.com/frenzymath/REAL-Prover"><img src="https://img.shields.io/badge/GitHub-REAL--Prover-blue.svg" alt="REAL-Prover"></a>
+    <a href="https://choosealicense.com/licenses/apache-2.0/"><img src="https://img.shields.io/badge/License-Apache%202.0-blue.svg" alt="License: Apache 2.0"></a>
+    <a href="https://leanprover-community.github.io/"><img src="https://img.shields.io/badge/Lean-4-orange" alt="Lean 4"></a>
+  </div>
+</div>
+
+## 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**
+
+
+## Associated Paper
+
+**REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning**  
+[arXiv:2505.20613](https://arxiv.org/abs/2505.20613)
+## Running Experiments
+**Repository**: [https://github.com/frenzymath/REAL-Prover](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.
+
+### Start Leansearch-PS-inference server
+See the detailed documentation in [LeanSearch-PS-inference/README.md](../LeanSearch-PS-inference/README.md).
+
+
+### Running
+
+
+
+Create a runtime configuration file (in TOML format) in `./experiment/examples/`, then run:
+
+```bash
+cd Realprover
+python -m experiment.run /path/to/config.toml
+```
+
+## Citation
+
+```bibtex
+@article{shen2025realproverretrievalaugmentedlean,
+      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}, 
+}