使用像 Lean 这样的计算机可验证形式化语言证明数学定理对数学推理具有重大影响。一种形式化定理证明方法涉及使用基于自然语言 (NL) 证明的大型语言模型 (LLM) 生成完整的证明。然而，由于对齐的 NL 和形式化语言 (FL) 定理证明数据的稀缺，大多数现代 LLM 表现出次优性能。这种稀缺导致用于训练 LLM 的方法和充分利用其在编写形式化证明方面的能力的技术匮乏。为了应对这些挑战，本文提出了 TheoremLlama，这是一个端到端框架，用于训练一个通用的 LLM 成为 Lean4 专家。TheoremLlama 包括 NL-FL 数据集生成和引导方法以获得对齐的数据集，课程学习和块训练技术来训练模型，以及迭代证明编写方法来编写协同工作的 Lean4 证明。使用 TheoremLlama 中的数据集生成方法，我们提供了开放引导定理 (OBT)，这是一个 NL-FL 对齐和引导数据集。我们新颖的 NL-FL 引导方法将 NL 证明集成到 Lean4 代码中以用于训练数据集，利用了 LLM 的 NL 推理能力进行形式化推理。TheoremLlama 框架在 MiniF2F-Valid 和 Test 数据集上分别实现了 36.48% 和 33.61% 的累积准确率，超过了 GPT-4 的 22.95% 和 25.41% 的基线。我们的代码、模型检查点和生成的数据集已发布在 GitHub 上。