Proof Verification Is Obligation Coverage: Pessimistic Checking of Open-Ended Mathematical Proofs

Open-ended proof verification is asymmetric: re- jection needs one faithful fatal obstruction, while acceptance requires all necessary theorem pre- conditions, case splits, witness bridges, imported dependencies, and conclusion-support links to be discharged. Existing verifier scaling samples more critiques or finer text chunks, but leaves this universal acceptance object implicit. We in- troduce Obligation-Covered Pessimistic Verifica- tion (OC-PVerify), an implemented verifier that extracts high-risk semantic obligations, checks them under first-error-wins pessimism, validates negative certificates for proof-faithfulness, and optionally audits whether uncovered fatal obliga- tions remain. On IMO-GradingBench, the ma- ture progressive baseline remains strongest on the 300-sample response-level run at 90.0% ac- curacy, but OC-PVerify changes the error profile: provenance-gated OC-PVerify improves the first- 50 split from 84.0% to 92.0% accuracy and from 0.826 to 0.920 F1, while a separate full-credit au- dit reaches 96.0% accuracy with zero false accepts under rubric context. The contribution is a new verification target, not a prompt stack: proof ac- ceptance as obligation coverage, with pessimistic verification recovered as risk-controlled search for a minimal witness of non-coverage.