DeepSeek-Prover-V1.5を紹介する。これはLean 4における定理証明を目的としたオープンソース言語モデルであり、DeepSeek-Prover-V1をさらに最適化した学習および推論プロセスを特徴とする。本モデルは、形式的数学言語に特化したDeepSeekMath-Baseで事前学習された後、DeepSeek-Prover-V1から抽出・拡張された形式的定理証明データセットを用いた教師あり微調整を経て、さらに証明支援ツールからのフィードバックを用いた強化学習（RLPAF）により精緻化されている。DeepSeek-Prover-V1が単一パスによる全体証明生成に依拠していたのに対し、本研究では、内在的報酬を駆動とする探索戦略を採用したモンテカルロ木探索（MCTS）の変種であるRMaxTSを提案し、多様な証明経路の生成を実現している。DeepSeek-Prover-V1.5は、DeepSeek-Prover-V1に比べて顕著な性能向上を示し、高校レベルのminiF2Fベンチマーク（テストセット）において63.5%の新記録、大学レベルのProofNetベンチマークにおいて25.3%の新記録を達成した。