Update README.md

README.md

@@ -1,15 +1,25 @@
----
-license: apache-2.0
----
-
-# LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
-
-This repository contains the model used in the paper *"LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation"*.
-
-## Model
-
-The model is full-tuned based on [Qwen2.5-Math-7B](https://huggingface.co/Qwen/Qwen2.5-Math-7B).
-
-## Usage
-
+---
+license: apache-2.0
+datasets:
+- internlm/Lean-Workbook
+language:
+- en
+base_model:
+- Qwen/Qwen2.5-Math-7B
+tags:
+- lean4
+- theorem-proving
+- formal-mathematics
+---
+
+# LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
+
+This repository contains the model used in the paper *"LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation"*.
+
+## Model
+
+The model is full-tuned based on [Qwen2.5-Math-7B](https://huggingface.co/Qwen/Qwen2.5-Math-7B).
+
+## Usage
+
 Please refer to [GitHub page](https://github.com/NJUDeepEngine/llm_based_atp) for details.