Update README.md

README.md

@@ -26,7 +26,7 @@ tags:
   </div>
 </div>
 
-## Overview
+## 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.
 
@@ -37,11 +37,12 @@ Our approach introduces several innovations:
 - Evaluations on both **ProofNet** and our proposed benchmark **FATE-M**
 
 
-## Associated Paper
+## 2. Associated Paper
 
 **REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning**  
 [arXiv:2505.20613](https://arxiv.org/abs/2505.20613)
-## Running Experiments
+
+## 3. Running Experiments
 **Repository**: [https://github.com/frenzymath/REAL-Prover](https://github.com/frenzymath/REAL-Prover)
 
 ### Input Data Format
@@ -63,7 +64,7 @@ cd Realprover
 python -m experiment.run /path/to/config.toml
 ```
 
-## Citation
+## 4. Citation
 
 ```bibtex
 @article{shen2025realproverretrievalaugmentedlean,