近年、大規模言語モデル（LLM）は厳密な数学的証明の生成において顕著な進展を遂げている。一方で、形式的言語（例：Lean）における定理証明にLLMを活用することは依然として困難であり、計算コストも非常に高くなる傾向にあり、特に大学レベル以上の問題に対しては顕著である。本研究では、大規模なエージェント型強化学習（agentic reinforcement learning）により訓練された形式的定理証明モデル「Seed-Prover 1.5」と、効率的なテスト時スケーリング（Test-Time Scaling: TTS）ワークフローを提案する。Leanをはじめとする各種ツールとの広範な相互作用を通じて、モデルは強化学習プロセス中に継続的に経験を蓄積し、形式的定理証明の能力と効率を著しく向上させた。さらに、自然言語による証明の最新の進展を活用することで、本TTSワークフローは自然言語と形式言語の間のギャップを効率的に埋めることに成功した。最先端の手法と比較して、Seed-Prover 1.5はより少ない計算リソースで優れた性能を達成しており、PutnamBench（大学レベル）の88％、Fate-H（大学院レベル）の80％、Fate-X（博士課程レベル）の33％の問題を正解した。特に、本システムを用いて、Putnam 2025の12問中11問を9時間以内に解くことに成功した。これらの結果から、高品質な形式的フィードバックに基づく経験からのスケーリング学習が、将来の形式的数学的推論の発展に極めて大きな可能性を秘めていることが示唆される。