Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

Abstract

Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems requiring complex mathematical reasoning, current systems rarely succeed on the first try and must repeatedly modify their proof strategies. Existing approaches for handling failed attempts typically either discard the entire proof and regenerate it from scratch or iteratively fix errors within the proof. The former is inefficient, as it may abandon mostly correct reasoning due to localized errors, while the latter, although preserving prior progress, leads to progressively longer contexts which progressively degrades the model's ability to attend to the remaining unresolved subproblems. To address this dilemma, we propose Mechanic, a novel agent system that employs a sorry-driven formal decomposition strategy. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, Mechanic extracts each failed subproblem into a clean, self-contained context and resolves it independently. This avoids both the waste of full regeneration and the excessive context length induced by repeated repairs. Experimental results on challenging mathematical competition benchmarks, including IMO 2025 and Putnam 2025, demonstrate that our agent achieves significant advantages in proving efficiency.

Figures (5)

• Figure 1: Comparison between informal and formal decomposition. (a) When a formal proof contains an error, previous approaches typically revert to an informal sketch and decompose the problem at the natural-language level, producing three subgoals in this example. (b) In contrast, our method identifies the incorrect block in the formal proof (highlighted in red). Replacing this block with the sorry placeholder yields a sorried proof. Each sorry can be extracted as a new subgoal. In this example, our pipeline requires only one subgoal.
• Figure 2: Workflow of Mechanic. (1) An informal solution is generated, verified and iteratively improved through a feedback loop. (2) The final informal solution is then translated into a formal proof, which is further revised based on Lean’s feedback. (3) If the proof continues to fail after several revisions, it is transformed into a sorried proof to extract subgoals. (4) Each resulting subgoal is subsequently handled by the same pipeline.
• Figure 3: Example of the subgoal splitting workflow. The proof is first verified by Lean (red block, step 1), and the Sorrifier replaces erroneous parts with sorry placeholders. The goal state of each sorry position is extracted, then converted into new subtheorems (orange blocks, step 2). After a subtheorem is proved, it is integrated back into the original proof at the corresponding location using apply tactic (green text, step 3).
• Figure 4: Number of nodes in different depth of the proof tree of IMO 2025 P4. The tree of Mechanic is wide but shallow, while others' are relatively deep.
• Figure 5: Proof tree of the IMO 2025 P3 and P5. The innermost node is the root nodes. Outer small sectors of each sector is the child nodes of that node. The proof tree generated by Mechanic is wide but relatively shallow.