---
license: apache-2.0
datasets:
- SJTULean/LeanStatement_CoT
language:
- en
base_model:
- Qwen/Qwen2.5-7B-Instruct
---

Wishing users to be clear that the model's formalization ability is (contrastivelty) relatively faible compared to LeanStatement_SFT and PPO, thus may only be considered as an experimental model.