---
license: apache-2.0
datasets:
- internlm/Lean-Workbook
language:
- en
base_model:
- Qwen/Qwen2.5-Math-7B
tags:
- lean4
- theorem-proving
- formal-mathematics
metrics:
- accuracy
pipeline_tag: text-generation
---

# 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.