Wir stellen DeepSeek-Prover-V1.5 vor, ein quelloffenes Sprachmodell, das für den Beweis von Sätzen in Lean 4 entwickelt wurde und sowohl die Trainings- als auch die Inferenzprozesse von DeepSeek-Prover-V1 optimiert. Das Modell wurde auf DeepSeekMath-Base vorgefertigt und spezialisiert auf formale mathematische Sprachen. Es durchläuft eine überwachte Feinabstimmung unter Verwendung eines verbesserten Datensatzes für formales Satzbeweisen, der aus DeepSeek-Prover-V1 abgeleitet ist. Eine weitere Verbesserung wird durch das Reinforcement Learning from Proof Assistant Feedback (RLPAF) erreicht. Neben dem Einzeldurchgang-Ansatz zur vollständigen Beweiserstellung von DeepSeek-Prover-V1 schlagen wir RMaxTS vor, eine Variante der Monte-Carlo-Baumsuche, die eine intrinsik-belohnungsgetriebene Explorationsstrategie verwendet, um vielfältige Beweiswege zu generieren. DeepSeek-Prover-V1.5 zeigt erhebliche Verbesserungen im Vergleich zu DeepSeek-Prover-V1 und erreicht neue Standartwerte auf dem Testset des Gymnasialniveaus miniF2F-Benchmarks (63,5 %) sowie des Hochschulniveaus ProofNet-Benchmarks (25,3 %).