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.

翻译：大语言模型（LLM）及基于LLM的智能体在自动定理证明领域取得了显著进展。然而，对于需要复杂数学推理的问题，现有系统很少能一次性成功，必须反复修改证明策略。当前处理失败尝试的方法通常要么完全丢弃证明并从头生成，要么迭代修复证明中的错误。前者效率低下，因为局部错误可能导致放弃大部分正确的推理；后者虽然保留了已有进展，但会导致上下文逐渐变长，从而降低模型处理剩余未解决子问题的能力。为解决这一困境，我们提出Mechanic，一种采用歉意驱动的形式化分解策略的新型智能体系统。通过利用Lean中的歉意占位符精确隔离未解决的子目标，同时保留已验证的证明结构，Mechanic将每个失败的子问题提取为清晰、独立的上下文，并独立求解。这既避免了完全重来的浪费，也避免了反复修复导致的上下文过长问题。在IMO 2025和Putnam 2025等具有挑战性的数学竞赛基准上的实验结果表明，我们的智能体在证明效率方面具有显著优势。