大規模言語モデル（LLMs）は、長時間の思考過程（long chain-of-thought）を用いた強化学習により、強力な数学的推論能力を示してきた。しかし、自然言語のみを用いる場合、定理証明において明確な教師信号が欠如しているため、依然として困難を抱えている。専用のドメイン特化言語であるLeanは、証明の形式的検証を通じて明確な教師信号を提供するため、強化学習を用いた効果的な学習を可能にしている。本研究では、証明全体をレムマ（lemma）スタイルで扱う統合的証明推論モデル「Seed-Prover」を提案する。Seed-Proverは、Leanからのフィードバック、既に証明されたレムマ、および自己要約に基づいて、反復的に証明を精緻化することができる。国際数学オリンピック（IMO）レベルの問題を解くために、推論時の3種類の推論戦略を設計し、深い理解と広範な探索の両方を実現している。Seed-Proverは、形式化された過去のIMO問題の78.1％を証明し、MiniF2Fの上限性能に達し、PutnamBenchでは50％以上を達成するという成果を上げ、従来の最先端手法を大きく上回った。さらに、Leanにおける幾何学的推論の不足に対応するため、幾何学的推論エンジン「Seed-Geometry」を導入した。このエンジンは、従来の形式的幾何学推論エンジンを上回る性能を発揮した。本研究では、これらの2つのシステムを用いてIMO 2025に参加し、6問中5問を完全に証明した。本研究は、形式的検証と長時間の思考過程を組み合わせた自動数学推論の分野において、顕著な進展を示しており、その有効性を実証した。