大语言模型（LLMs）通过结合长链式思维（long chain-of-thought）与强化学习，已展现出强大的数学推理能力，但在定理证明方面仍面临挑战，主要原因在于仅依赖自然语言时缺乏清晰的监督信号。专用领域特定语言（如 Lean）通过形式化证明验证提供明确的监督信号，从而支持基于强化学习的有效训练。在本工作中，我们提出 Seed-Prover——一种基于引理风格的完整证明推理模型。Seed-Prover 能够根据 Lean 的反馈、已证明的引理以及自我总结，迭代优化其证明过程。为解决国际数学奥林匹克（IMO）级别的竞赛题，我们设计了三种测试时推理策略，实现深度与广度兼具的推理能力。实验结果表明，Seed-Prover 成功证明了 78.1% 的形式化历史 IMO 问题，完全解决 MiniF2F 基准，且在 PutnamBench 上取得超过 50% 的成绩，显著超越此前的最先进方法。针对 Lean 在几何推理方面支持不足的问题，我们进一步提出几何推理引擎 Seed-Geometry，其性能优于以往的形式化几何推理系统。我们利用上述两个系统参与 2025 年国际数学奥林匹克竞赛，并成功完整证明了其中 5 道题目。本工作标志着自动化数学推理领域的重要进展，充分验证了结合形式化验证与长链式思维推理的有效性。