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

• URL: http://arxiv.org/abs/2603.24465v1
• Date: Wed, 25 Mar 2026 16:12:08 GMT
• Title: Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
• Abstract summary: Mechanic is a novel agent system that employs a sorry-driven formal decomposition strategy.<n>By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals, Mechanic extracts each failed subproblem into a clean, self-contained context and resolves it independently.
• Score: 13.446180044466324
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization [20.22828310618122]
  ToMap is a framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline.<n>We show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness.
  arXiv  Detail & Related papers  (2026-07-13T09:21:15Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• VerifyMAS: Hypothesis Verification for Failure Attribution in LLM Multi-Agent Systems [79.51005192758262]
  Large language model-driven multi-agent systems excel at complex tasks.<n>However, unreliable agents remain a key bottleneck to system-level reliability.<n>We propose a hypothesis verification framework for agent failure attribution.
  arXiv  Detail & Related papers  (2026-05-17T14:09:35Z)
• Dynamic analysis enhances issue resolution [53.50448142467294]
  DAIRA (Dynamic Analysis-enhanced Issue Resolution Agent) is an automated repair framework that embeds dynamic analysis into the agent's reasoning cycle.<n> Driven by a Test Tracing-Driven methodology, DAIRA utilizes lightweight monitors to extract critical runtime data.<n>When powered by Gemini 3 Flash Preview, DAIRA establishes a new state-of-the-art (SOTA) performance, achieving a 79.4% resolution rate on the SWE-bench Verified dataset.
  arXiv  Detail & Related papers  (2026-03-23T14:48:54Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  We propose a self-consistency framework that turns cheap diffusion-sampled reasoning into a reusable pool of step-level candidates.<n>We find that step-level recombination is most beneficial on harder problems.<n>Our training-free framework improves average accuracy by up to 2 across six math and coding tasks.
  arXiv  Detail & Related papers  (2026-02-26T11:08:39Z)
• Decompose-and-Formalise: Recursively Verifiable Natural Language Inference [34.505373718498014]
  Large language models (LLMs) with theorem provers (TPs) in neuro-symbolic pipelines helps with entailment verification and proof-guided refinement of explanations for natural language inference (NLI)<n>We propose a decompose-and-formalise framework that decomposes premise-hypothesis pairs into an entailment tree of atomic steps.<n>We also introduce $$-substitution in an event-based logical form to enforce consistent argument-role bindings.
  arXiv  Detail & Related papers  (2026-01-27T13:43:30Z)
• Gödel's Poetry [0.0]
  We introduce a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation.<n>We achieve a 90.4% pass rate on miniF2F without decomposition.<n>A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities.
  arXiv  Detail & Related papers  (2025-12-16T10:00:01Z)
• Metacognitive Self-Correction for Multi-Agent System via Prototype-Guided Next-Execution Reconstruction [58.51530390018909]
  Large Language Model based multi-agent systems excel at collaborative problem solving but remain brittle to cascading errors.<n>We present MASC, a metacognitive framework that endows MAS with real-time, unsupervised, step-level error detection and self-correction.
  arXiv  Detail & Related papers  (2025-10-16T05:35:37Z)
• Accelerating LLM Reasoning via Early Rejection with Partial Reward Modeling [12.835376812101323]
  We introduce the hypothesis that PRMs are also Partial Reward Models.<n>This allows for principled early rejection based on intermediate token-level signals.<n>On math reasoning benchmarks, our method achieves up to 1.4$times$-9$times$ reduction in inference FLOPs without degrading final performance.
  arXiv  Detail & Related papers  (2025-08-04T00:58:56Z)
• Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
  Recent studies show that the informal accuracy exceeds 80% while formal success remains below 8% on benchmarks like PutnamBench.<n>We propose a novel framework that decouples high-level reasoning from low-level proof generation.<n>We evaluate our method on a challenging set of post-2000 IMO problems, a problem set on which no prior open-source prover has reported success.
  arXiv  Detail & Related papers  (2025-07-07T22:38:49Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  We present APOLLO (Automated PrOof repair viaLLM and Lean cOllaboration), a model-agnostic agentic framework for automated theorem proving.<n>A set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal.<n>Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness.
  arXiv  Detail & Related papers  (2025-05-09T03:38:31Z)
• A Theoretical Analysis of the Repetition Problem in Text Generation [55.8184629429347]
  We show that the repetition problem is, unfortunately, caused by the traits of our language itself. One major reason is attributed to the fact that there exist too many words predicting the same word as the subsequent word with high probability. We propose a novel rebalanced encoding approach to alleviate the high inflow problem.
  arXiv  Detail & Related papers  (2020-12-29T08:51:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.