Closing the Loop in Formal Theorem Proving: Coordinated and Revisable Proof Construction

Agentic theorem provers increasingly combine mathematical reasoning, proof decomposition, and iterative interaction with Lean. When proof construction stalls, the underlying difficulty may arise in formal proving, the informal proof strategy, or the surrounding proof structure, and Lean's diagnostics alone do not identify which source is responsible. Effective recovery requires identifying the source of difficulty and controlling the scope of revision. We present OpenMathHarness (OMH), an agentic theorem-proving framework that coordinates decomposition, informal reasoning, formal proving, and revision within a unified proof construction process. OMH introduces a multi-level review mechanism that uses formal evidence to direct subsequent recovery effort to formal refinement, revision of the informal proof strategy under a fixed statement, or structural revision. Using DeepSeek-V4-Flash as its backbone, OMH solves 53/100 problems on FATE-X and 11/12 on Putnam 2025, at mean inference costs of $1.23 and $0.27 per solved problem respectively. Controlled experiments show that decomposition and informal guidance improve performance on effort-intensive problems, and strategy flexibility nearly halves token usage on commonly solved nodes. Analysis of review and routing decisions further shows how recovery unfolds across formal, strategy, and structural levels.