Learning to Solve Step-Level Proof Gaps via Post-Training

ProofGap introduces a new step-level formal reasoning task: solving local proof obligations aligned with semantic steps of natural-language solutions. By separating local proof construction from end-to-end theorem proving, this task provides finer-grained assessment of formal reasoning and motivates dedicated post-training research. We develop gap-specific post-training, aiming to solve these obligations more cost-effectively than transferring theorem-level training recipes to the same task. We also study how post-training can teach models the Domain Specific Language (DSL) introduced with ProofGap, a formal proof language unseen by the base models during pretraining. Our method uses a three-role architecture: natural-language drafting for formal proofs, DSL translation that can revise unreliable drafts, and model correction using verifier diagnostics. The drafting model remains frozen, while the translation and correction models receive task-specific post-training. These roles connect local mathematical intent to executable evidence and target efficient learning of the new language. On 4,000 gaps sampled from the ProofGap benchmark, none of which are solved by direct autosolve, our full system achieves a gap-level success rate of 35.70%, compared with 25.0% for the Codex baseline under the same theorem library and verifier, an improvement of 10.70 percentage points.