OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

Recent advances in formal theorem proving have focused on Olympiad-level mathematics, leaving undergraduate domains largely unexplored. Optimization, fundamental to machine learning, operations research, and scientific computing, remains underserved by existing provers. Its reliance on domain-specific formalisms (convexity, optimality conditions, and algorithmic analysis) creates significant distribution shift, making naive domain transfer ineffective. We present OptProver, a trained model that achieves robust transfer from Olympiad to undergraduate optimization. Starting from a strong Olympiad-level prover, our pipeline mitigates distribution shift through two key innovations. First, we employ large-scale optimization-focused data curation via expert iteration. Second, we introduce a specialized preference learning objective that integrates perplexity-weighted optimization with a mechanism to penalize valid but non-progressing proof steps. This not only addresses distribution shifts but also guides the search toward efficient trajectories. To enable rigorous evaluation, we construct a novel benchmark in Lean 4 focused on optimization. On this benchmark, OptProver achieves state-of-the-art Pass@1 and Pass@32 among comparably sized models while maintaining competitive performance on general theorem-proving tasks, demonstrating effective domain transfer without catastrophic forgetting.

We present OptProver, a trained model to solve undergraduate-level optimization problems, a core area in machine learning, operations research, and scientific computing. While recent AI theorem provers have focused mainly on competition-style mathematics, important undergraduate domains such as optimization remain relatively unexplored. OptProver builds on a strong competition-level prover and adapts it to optimization through two key components: large-scale optimization-focused training data and a learning strategy that encourages efficient proof search. To support rigorous evaluation, we also introduce a new Lean 4 benchmark for optimization. Compared with models of similar size, OptProver achieves state-of-the-art performance on this benchmark while remaining competitive on general theorem-proving tasks, showing that theorem provers can successfully transfer their problem-solving abilities to new mathematical domains.