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

1. Problem Statement

Automated theorem proving (ATP) using Large Language Models (LLMs) has made significant strides, particularly in formal languages like Lean. However, current systems face a critical bottleneck when handling complex, long-horizon reasoning tasks:

• Inefficiency of Full Regeneration: When a proof attempt fails, existing agents often discard the entire proof and restart from scratch (informal decomposition). This wastes computational resources and discards valid, verified portions of the proof.
• Context Degradation in Iterative Repair: Alternatively, agents may attempt to iteratively fix errors within the existing proof. However, as errors accumulate and are patched, the context length grows significantly. This degrades the model's ability to attend to unresolved subproblems, leading to diminishing returns.
• The "Cascading Error" Phenomenon: In dependent type systems like Lean, a single logical flaw in a local block often corrupts the entire local context, causing a cascade of false errors in subsequent, otherwise correct code. Naive error fixing often deletes too much valid code to resolve these cascades.

2. Methodology: The Mechanic Agent

The authors propose Mechanic, a novel agent system that introduces a Sorrifier-Driven Formal Decomposition strategy. Instead of discarding failed proofs or blindly iterating repairs, Mechanic surgically isolates errors while preserving the surrounding verified structure.

Core Components

1. Specialized LLMs:
   • Reasoner: Generates informal proof sketches and synthesizes premises for subgoals.
   • Verifier: Evaluates the logical soundness of informal proofs, formal strategies, and extracted subgoals.
   • Prover: Translates informal sketches into Lean and revises proofs based on compiler feedback.
2. Lean Toolkit: Includes the Lean compiler for verification and search tools (LeanDex, Loogle) for retrieving relevant theorems from Mathlib.
3. The Sorrifier (Core Innovation): A specialized module that transforms a failing Lean proof into a "sorried proof" (a syntactically valid but incomplete proof) by replacing erroneous blocks with the sorry placeholder.

The Workflow

The Mechanic pipeline follows a four-step iterative process:

1. Informal Prove: The Reasoner generates an informal proof sketch, which is refined through a feedback loop with the Verifier until logically sound.
2. Formal Prove: The Prover translates the sketch into Lean. If the compiler rejects it, the Prover attempts error correction based on compiler feedback and Verifier comments.
3. Subgoal Split (The Sorrifier Phase): If the proof fails after several repair attempts, the Sorrifier takes over:
   • Surgical Isolation: It identifies the innermost reported error. If the error is inside a have block, it replaces only that block with sorry. If outside, it truncates the code at the error line and appends sorry.
   • Recompilation: The code is immediately recompiled. This step is crucial as it removes downstream "cascading errors" caused by the initial flaw, preventing the deletion of valid code.
   • Extraction: Each sorry placeholder is extracted as a self-contained subgoal. The Reasoner identifies relevant hypotheses from the local context to formulate a clean lemma.
   • Validation: The Verifier performs syntactic and semantic checks on the extracted subgoals to ensure they are well-formed and logically sound (preventing infinite loops or impossible goals).
4. Subgoal Process: Each extracted subgoal is processed recursively using the same pipeline. Once proven, the subgoal is reassembled into the main proof using an apply tactic, replacing the sorry.

3. Key Contributions

• Sorrifier-Driven Decomposition: The paper introduces a method to decompose formal proofs without discarding verified progress. By leveraging the sorry placeholder, it isolates localized errors, transforming a monolithic failure into manageable, independent subproblems.
• Handling Cascading Errors: The iterative, innermost-error-targeting algorithm effectively mitigates the "cascading error" problem in dependent type systems, ensuring that only the minimal necessary code is replaced.
• Hybrid Informal-to-Formal Pipeline: The system effectively bridges natural language reasoning with formal verification, using informal sketches to guide the structure while relying on formal decomposition to resolve specific logical gaps.
• Efficiency in Long-Horizon Reasoning: By keeping proof trees "wide but shallow" (parallelizable subgoals) rather than "deep and narrow" (sequential, nested repairs), the system significantly reduces the context length required for the LLM.

4. Experimental Results

The authors evaluated Mechanic on challenging mathematical benchmarks: Putnam 2025 (12 problems) and IMO 2025 (4 problems).

• Performance:
  • Putnam 2025: Mechanic solved 11 out of 12 problems. It outperformed state-of-the-art baselines (Hilbert, Aristotle, Axiom, Seed-Prover, Numina) in all metrics for the solved problems.
  • IMO 2025: Mechanic demonstrated superior efficiency, particularly on harder problems. On Problem P1, it ran in roughly one-third of the time required by the Seed-Prover baseline.
• Efficiency Metrics:
  • Time & Cost: Mechanic achieved an average runtime of 114 minutes and an API cost of $18.5 for Putnam 2025, significantly lower than competitors.
  • Proof Complexity: The generated proofs were shorter (fewer lines) and required fewer auxiliary lemmas (smaller proof trees) compared to baselines.
  • Tree Structure: Analysis showed Mechanic's proof trees are wide and shallow, allowing for parallel processing of subgoals, whereas other methods produced deep, sequential trees that increased latency.

5. Significance

This work represents a paradigm shift in automated theorem proving from "regenerate-and-retry" to "isolate-and-resolve."

• Resource Efficiency: It drastically reduces the computational cost and time required to prove complex theorems by reusing verified code segments.
• Scalability: The approach addresses the context window limitations of LLMs by breaking down complex proofs into smaller, independent contexts, making it more scalable for research-level mathematics.
• Robustness: The ability to surgically fix errors without breaking the surrounding proof structure makes the system more robust against the fragility of LLM-generated code in formal environments.

In conclusion, Mechanic demonstrates that leveraging formal language features (like sorry) for structural decomposition is a highly effective strategy for overcoming the limitations of current LLM-based theorem provers in complex reasoning tasks.