---
license: apache-2.0
datasets:
- SJTULean/LeanStatement_CoT
language:
- zho
- eng
- fra
- spa
- por
- deu
- ita
- rus
- jpn
- kor
- vie
- tha
- ara
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.