Proof assistants like Lean have revolutionized mathematical proof
verification, ensuring high accuracy and reliability. Although large language
models (LLMs) show promise in mathematical reasoning, their advancement in
formal theorem proving is hindered by a lack of training data. To address this
issue, we introduce an approach to generate extensive Lean 4 proof data derived
from high-school and undergraduate-level mathematical competition problems.
This approach involves translating natural language problems into formal
statements, filtering out low-quality statements, and generating proofs to
create synthetic data. After fine-tuning the DeepSeekMath 7B model on this
synthetic dataset, which comprises 8 million formal statements with proofs, our
model achieved whole-proof generation accuracies of 46.3% with 64 samples and
52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at
23.0% with 64 samples and a tree search reinforcement learning method at 41.0%.
Additionally, our model successfully proved 5 out of 148 problems in the Lean 4
Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4
failed to prove any. These results demonstrate the potential of leveraging
large-scale synthetic data to enhance theorem-proving capabilities in LLMs.
Both the synthetic dataset and the model will be made available to facilitate
further research in this promising field.

基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。