大型语言模型（LLM）近年来在生成严谨数学证明方面取得了显著进展。然而，将这些模型应用于形式化语言（如Lean）中的定理证明，仍面临巨大挑战，且计算成本高昂，尤其是在处理本科及以上水平的数学问题时。在本研究中，我们提出了Seed-Prover 1.5，这是一个通过大规模智能体强化学习（agentic reinforcement learning）训练而成的形式化定理证明模型，并配套设计了一种高效的测试时扩展（Test-Time Scaling, TTS）工作流。通过与Lean及其他工具进行大量交互，模型在强化学习过程中持续积累经验，显著提升了形式化定理证明的能力与效率。此外，借助自然语言证明领域的最新进展，我们的TTS工作流能够高效弥合自然语言与形式语言之间的鸿沟。相较于现有最先进方法，Seed-Prover 1.5在更小的计算资源消耗下实现了更优性能：在本科水平的PutnamBench基准上解决了88%的问题，在研究生水平的Fate-H上解决了80%，在博士水平的Fate-X上解决了33%的问题。尤为值得一提的是，利用本系统，我们在9小时内成功解决了2025年普特南数学竞赛（Putnam 2025）中12道题目中的11道。我们的研究结果表明，基于高质量形式化反馈驱动的经验积累式学习，具有巨大的潜力，有望推动形式化数学推理的未来发展。