internlm/Lean-Workbook
Viewer • Updated • 25.2k • 652 • 56
This repository contains the model used in the paper "LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation".
The model is full-tuned based on Qwen2.5-Math-7B.
Please refer to GitHub page for details.