Editable Proof Sketch for Automated Theorem Proving

As large language models (LLMs) improve in mathematical reasoning and formal understanding, a promising approach for automated theorem proving (ATP) is to enable LLMs construct proof sketches, which plan a high-level proof strategy and decompose complex theorems into independently provable subgoals. However, most existing proof sketches are immutable. As a result, any revision typically requires rebuilding the entire sketch, which discards already proved subgoals and bring additional cost. In this paper, we address this limitation by introducing EditableSketch, an editable proof-sketch structure that supports in-place edits for error correction and further subgoal decomposition while preserving previously proved subgoals. Building on EditableSketch, we introduce SketchRefine, a proof-generation framework for ATP by iteratively refining proof sketches through localized, incremental edits. Experiments show that our method not only reduces the cost of the proof process, but also achieves superior performance. For example, our method realizes 76.0% pass rate on FormalMath-Lite (+14.1\% vs. DeepSeek-Prover-V2-671B). Meanwhile, compared with Hilbert, our method significantly reduces token overhead while achieving comparable performance.

Computers are becoming better at checking mathematical proofs, but automatically finding those proofs is still difficult. A common approach is to ask a large language model to first write a rough proof plan, then let a formal proof system fill in and verify the details. However, if one part of the plan is wrong or too hard, many existing systems need to rebuild the whole plan from scratch, wasting effort and losing already verified progress. We introduce EditableSketch, a way to write proof plans so that they can be edited locally, much like revising one paragraph in a document without rewriting the entire paper. Based on this idea, our system SketchRefine repairs wrong steps and breaks difficult steps into smaller ones while keeping the parts that have already been proved. This makes automated theorem proving more efficient and more successful, helping AI systems produce reliable, machine-checked mathematical proofs.