internlm/Lean-Workbook
Viewer โข Updated โข 25.2k โข 3k โข 61
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.