大型语言模型 (LLM) 在与 Lean 等交互式证明助手集成后，在形式化定理证明等数学推理任务中取得了成功。现有的方法涉及在特定数据集上训练或微调 LLM，以在特定领域（如本科数学）中表现良好。这些方法在泛化到高级数学方面存在困难。一个根本的限制是这些方法在静态领域中运行，无法捕捉到数学家如何经常在多个领域和项目之间同时或循环地工作。我们提出了 LeanAgent，这是一种用于定理证明的新型终身学习框架，它能够不断地泛化到不断扩展的数学知识并改进其知识，而不会忘记之前学到的知识。LeanAgent 引入了几个关键创新，包括一种课程学习策略，该策略根据数学难度优化学习轨迹；一个用于有效管理不断发展的数学知识的动态数据库；以及渐进式训练，以平衡稳定性和可塑性。LeanAgent 成功证明了来自 23 个不同 Lean 库（其中许多来自高级数学）的 162 个以前人类无法证明的定理。它的性能比静态 LLM 基线高出 11 倍，证明了诸如抽象代数和代数拓扑等领域中的挑战性定理，同时展示了从基本概念到高级主题的清晰学习过程。此外，我们分析了 LeanAgent 在关键终身学习指标上的优异表现。LeanAgent 在稳定性和反向迁移方面取得了非凡的成绩，其中学习新任务可以提高对先前学习任务的性能。这强调了 LeanAgent 的持续泛化能力和改进能力，解释了其优异的定理证明性能。