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

Ruichen Qiu; Yichuan Cao; Junqi Liu; Dakai Guo; Xiao-Shan Gao; Lihong Zhi; Ruyong Feng

cs.CLMar 25, 2026

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

Authors: Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao, Lihong Zhi, Ruyong Feng

Organizations: SKLMS, Academy of Mathematics and Systems Science, CAS, Beijing, 100190, China · School of Advanced Interdisciplinary Sciences, UCAS, Beijing, 101408, China · School of Mathematical Science, UCAS, Beijing, 101408, China

Abstract

Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems that require complex mathematical reasoning, current systems seldom succeed in their initial attempt, necessitating iterative adjustments to their proof strategies. Existing approaches for handling failed attempts typically either iteratively fix errors within the proof or discard the entire proof and regenerate it from scratch. The former leads to progressively longer contexts, which degrade the model's ability to attend to the remaining unresolved subproblems, while the latter is inefficient, as it may abandon mostly correct reasoning due to localized errors. To address this dilemma, we present MechMath, an agent system centered on a Sorrifier-driven formal decomposition paradigm. By leveraging the sorry placeholder in Lean to precisely isolate unresolved subgoals while preserving the surrounding verified proof structure, MechMath 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, Putnam 2025, miniF2F, and a subset of ProverBench, demonstrate that our agent achieves significant advantages in proving efficiency.

Figures & tables

Panel of Figure 1 — Figure 1: Comparison between (a) informal and (b) formal decomposition. (a) Conventional approaches decompose the proof via an informal sketch, resulting in three subgoals. (b) Our method identifies the erroneous proof block and generates a sorried proof, from which we extract only one subgoal, minimizing decomposition overhead.

Panel of Figure 2 — Figure 2: Workflow of MechMath. (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).

Table 1: Putnam 2025 benchmark. (a) A single prover model or a general LLM cannot solve any problem within 32 attempts. (b) MechMath achieves high efficiency on 11 solved problems: shorter time expenditure (6/11), lower cost (10/11), and fewer theorem counts (8/11). The averages of Axiom and Numina are computed exclusive of A5.

Table 3: Ablation study. (b), (c) and (d) is conducted on MechMath-Hard, since the easy mode fails in most of these settings.

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Tactic	Functionality	Example Context
have	Introduces an intermediate assertion or lemma to the local context.	have h : n > 0 := ...
let	Defines a local term or function with a specific value.	let f := n + 1
apply	Matches the current goal with the conclusion of a theorem.	apply Nat.add_comm
exact	Closes a goal that matches a given term or hypothesis precisely.	exact h
intro	Moves a universal quantifier ( $\forall$ ) or premise ( $\to$ ) into the context.	intro n hn
cases	Performs case analysis on a hypothesis or inductive type.	cases h with \| hl \| hr

Appendix

Table 4: Fundamental Tactics for Formal Proof Construction in Lean.

Panel of Figure 5 — 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 MechMath is wide but relatively shallow.

	A1	A2	A3	A4	A5	A6	B1	B2	B3	B4	B5	B6	Avg
#Tokens (K)	175	531	1,209	1,912	-	836	1,660	663	898	871	2,732	484	1,088
#Sorrify	2	8	16	16	-	8	24	5	10	9	28	13	12.6
LLM Calls	7	35	73	92	-	41	143	59	110	85	302	57	91.3

Appendix

Table 5: Detailed inference costs and proof metrics across the problems resolved by MechMath on Putnam 2025.

	P1	P3	P4	P5	Avg
#Tokens (M)	13.77	4.81	8.34	5.04	7.99
#Sorrify	155	60	104	73	98.0
LLM Calls	981	450	726	417	643.5

Appendix

Table 6: Detailed inference costs and proof metrics across the problems resolved by MechMath on IMO 2025.

	A1	A2	A3	A4	A5	A6	B1	B2	B3	B4	B5	B6	Avg
Hilbert	-	-	-	-	-	-	-	-	1220	-	-	-	1220
Seed	631	469	927	1095	-	881	849	1613	584	628	2499	2594	1161
Axiom	556	458	1089	825	1878	468	1179	346	302	993	1310	862	763
Numina	365	401	422	605	3263	835	328	690	292	648	929	1820	667
MechMath-Easy	339	643	616	792	-	507	-	519	533	700	2022	-	741
MechMath-Hard	112	798	560	793	-	280	1425	224	627	568	1256	578	656

Appendix

Table 7: Proof length of the Putnam 2025 benchmark. The averages of Axiom and Numina are computed exclusive of A5.

Table 8: Pass rates on miniF2F and ProverBench-NT. MechMath achieves highly competitive performance with extremely low cost.

	# LLM Calls	# Total Tokens	Time (min)	Cost (USD)	# Lemmas	# Lean lines
Avg	57.6	549 K	62.1	4.66	4.9	232.4
Min	5	35 K	4.2	0.10	1	21
Max	512	4.73 M	353.9	42.47	36	1442

Appendix

Table 9: Detailed inference costs and proof metrics across the problems resolved by MechMath on miniF2F (exclude simple prombles).

Panel of Figure 6 — Figure 6: We compare the cumulative pass rate of MechMath against HILBERT as a function of four metrics per sample: (top left) total number of LLM calls, (top right) total token usage, (bottom left) time expenditure, and (bottom right) monetary cost. Note that since the raw data for HILBERT is not publicly available, their reference points are approximated by extracting values at key nodes directly from their original plots.

	# LLM Calls	# Total Tokens	Time (min)	Cost (USD)	# Lemmas	# Lean lines
Avg	45.2	336 K	28.8	2.97	4.25	166
Min	5	35 K	5.7	0.02	1	9
Max	216	1.62 M	145.6	14.89	19	536

Appendix

Table 10: Detailed inference costs and proof metrics across the problems resolved by MechMath on number theory subsets in ProverBench.

	IMO	AIME	AMC	Algebra	Number Theory	Induction	Overall
Subset	19 / 20	15 / 15	45 / 45	88 / 88	67 / 68	8 / 8	242 / 244

Appendix

Table 11: Pass rates across diverse categories on miniF2F

Error Type	Putnam 2025	IMO 2025	miniF2F	ProverBench
Syntax	0.61%	5.60%	0.41%	5.13%
Extraction	3.05%	4.85%	0.00%	1.92%
Logic	1.22%	1.49%	1.23%	7.05%

Appendix

Table 12: Quantitative breakdown of error types occurring across all generated subgoals across different benchmarks.

Automated Theorem Proving

Automated theorem proving develops algorithms and AI systems that construct or check formal proofs in mathematics, logic, and software.

See all 159 papers

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Jun 2, 2026Po-Nien Kung, Linfeng Song, Dawsen Hwang +10Mathematical Reasoning Benchmarks Large Language Model-Guided Theorem Proving
Google Cloud AI Research · Google Cloud · Google DeepMind
MechMath Agent Team: LLM Driven Agents for Mathematical Research
Jul 5, 2026Yichuan Cao, Ruichen Qiu, Junqi Liu +5Automated Theorem Proving Multi-Agent Reasoning
State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, CAS · School of Mathematical Sciences, University of Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences
Maestro: Agentic Formal Proof Development by Coordination
Oct 19, 2026Haoyu Li, Zeren Shui, Yuhao Zhang +4Large Language Model-Guided Theorem Proving Lean Theorem Proving
University of Illinois Urbana-Champaign · AWS AI Labs · Georgia Institute of Technology

Jun 2, 2026J/K move · Enter open · S save

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon+9

Google Cloud AI Research · Google Cloud · Google DeepMind

Mathematical Reasoning Benchmarks Large Language Model-Guided Theorem Proving Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Open paper AskPDF arXiv

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.

Abstract

Automated Theorem Proving

Explore similar work

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

MechMath Agent Team: LLM Driven Agents for Mathematical Research

Maestro: Agentic Formal Proof Development by Coordination