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

arXiv:2603.24465 · cs.CL · Submitted 2026-08-16 · Read on arXiv

Listen

Radio episode about this paper

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: Next we'll be talking about the paper "MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving".

Jane: The paper was written by Ruichen Qiu, Yichuan Cao, Junqi Liu, Dakai Guo, Xiao-Shan Gao et al. from Academy of Mathematics and Systems Science, Chinese Academy of Sciences and School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences and School of Mathematical Science, University of Chinese Academy of Sciences.

Tom: Stay tuned as we take you through the paper and discuss its implications.

Title: Tom: Welcome back to the channel, everybody. Today we’re digging into a paper that’s got a name you can’t forget: “Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving.” Jane, I gotta say, the word “Sorrifier” alone made me do a double take.

Jane: It really is a strange word, Tom, but it’s actually perfect once you understand what it does. In the Lean proof assistant, you can write the word “sorry” as a placeholder when you don’t know how to finish a proof yet. The computer accepts it temporarily, but it marks that spot as unfinished. The Sorrifier is a tool that takes a broken proof and strategically replaces the broken parts with those “sorry” placeholders, so the rest of the proof can still be checked.

Tom: So it’s like putting a bookmark in a book you can’t finish reading, instead of throwing the whole book away.

Jane: Exactly. And that’s the core idea of the whole paper. When an AI tries to prove a hard math problem, it often gets most of the way there and then hits one small error. Older systems would just scrap everything and start over, which is wasteful. Mechanic keeps the good parts and only makes you redo the bad parts.

Tom: And the authors are from the Academy of Mathematics and Systems Science in Beijing, plus a bunch of collaborators. They’ve got a big team, and they’re clearly serious about pushing automated theorem proving forward.

Jane: They are. And the implications here are pretty big. We’re not just talking about solving textbook exercises. They tested this on the two thousand twenty-five Putnam competition, which is one of the hardest undergraduate math contests in the world, and they solved eleven out of twelve problems. That’s a level of performance that would have been unthinkable a few years ago.

Tom: Eleven out of twelve? That’s insane. And they did it with a fraction of the time and money that other top systems needed.

Jane: Right. And that efficiency is exactly what we’re going to dig into next. Because it’s not just about whether you can solve the problem, it’s about how fast and how cheaply you can do it.

Tom: Well, I’m hooked. Let’s get into the details of how this workflow actually runs.

Summary: Tom: So Jane, we’ve got the title and the big idea. Now let’s talk about what this system actually does step by step, because the workflow is surprisingly human-like.

Jane: It really is. The system, Mechanic, works in four stages. First, it generates an informal proof sketch, the kind of thing a mathematician would write on a whiteboard. Then it tries to translate that sketch into a formal Lean proof. If the Lean compiler rejects it, the system doesn’t panic. It uses the Sorrifier to find the exact spot where the logic breaks and replaces just that piece with a “sorry” placeholder.

Tom: So instead of starting from zero, it surgically removes the tumor and leaves the healthy tissue intact.

Jane: That’s a good way to put it, Tom. Then it extracts that “sorry” spot as a new, smaller subgoal, proves that subgoal independently, and stitches it back into the main proof. If that subgoal is too hard, it can be split again, creating a tree of subgoals.

Tom: And this is where the efficiency comes from. On the Putnam two thousand twenty-five benchmark, Mechanic took about one hundred fourteen minutes per problem on average and cost about eighteen and a half dollars. Compare that to other systems like Hilbert or Axiom, which sometimes took hours and cost hundreds of dollars.

Jane: Right. And it’s not just about speed. The proofs Mechanic generates are shorter too. They averaged around six hundred fifty-six lines per proof, while other systems often produced proofs that were over a thousand lines long. The proof trees are also shallower, which means less waiting around for one subgoal to finish before the next one can start.

Tom: Shallow and wide beats tall and skinny, got it. But I have to ask, is this just because they used a really good language model, or is the workflow itself doing the heavy lifting?

Jane: That’s the million-dollar question, and they actually tested it. They ran the same pipeline with different language models, from Gemini to Claude to DeepSeek. The stronger models solved all the test problems, while the weaker ones struggled. So the model matters, but the workflow amplifies whatever model you have. Even the weaker models solved problems they couldn’t solve at all without the Mechanic pipeline.

Tom: So it’s like giving a good mechanic a better toolbox. The toolbox doesn’t replace the mechanic, but it makes them way more effective.

Jane: Exactly. And that’s the part that gets me excited, because it means this approach could work with any future model that comes out. You just plug it in and get better results.

Tom: Alright, so we know it works. But what’s actually new here compared to what people were doing before? Let’s talk about that in the next segment.

Improvements: Tom: So Jane, we’ve covered what Mechanic does and how fast it is. But what’s genuinely new here? What did they improve over the state of the art?

Jane: The key improvement is the philosophy of how to handle failure. Older systems like Hilbert or Axiom, when they hit an error, they go back to the informal sketch and re-decompose the whole problem in natural language. That’s wasteful because the formal proof might be ninety percent correct. Mechanic instead decomposes the problem formally, right inside the Lean code itself.

Tom: So they’re not just re-planning in English, they’re actually looking at the broken Lean code and figuring out the smallest piece that needs fixing.

Jane: Precisely. And there’s a subtle technical challenge they had to solve. In Lean, one small error can cause a cascade of fake errors downstream. If you tried to fix all of them at once, you’d delete huge chunks of valid proof. The Sorrifier works around this by targeting the innermost error first, fixing it, recompiling, and then moving to the next one. It’s a very careful, iterative process.

Tom: Like untangling a knot by pulling the loose end instead of cutting the whole rope.

Jane: That’s the idea. And they also added a safety valve. If a subgoal turns out to be impossible to prove, which can happen if the original proof strategy was flawed, the system detects that and goes back to trying to fix the whole proof instead of getting stuck in an infinite loop.

Tom: So it knows when to quit and try a different approach. That’s pretty mature behavior for an AI system.

Jane: It is. And the results speak for themselves. On the IMO two thousand twenty-five problems, which are even harder than Putnam, Mechanic solved four out of five problems they attempted. On the hardest one, Problem one it took about three hundred sixty-three minutes, while the previous best system, Seed, took nine hundred ninety minutes. That’s nearly three times faster.

Tom: Three times faster on the hardest problem. That’s not a small improvement, that’s a game changer.

Jane: And the proofs are cleaner too. The paper shows that Mechanic’s proof trees are wide and shallow, meaning it breaks problems into many small pieces that can be solved in parallel, rather than a few big pieces that have to be solved one after another.

Tom: So it’s not just faster, it’s also more parallelizable. That’s huge for scaling up to even harder problems.

Jane: Exactly. And that’s what we should be thinking about next. Where does this go from here?

Conclusion: Tom: Alright, we’ve covered the title, the workflow, and the improvements. Let’s wrap this up. Jane, what’s the big takeaway from “Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving”?

Jane: The big takeaway, Tom, is that we don’t need to throw away good work just because of a small mistake. Mechanic shows that by being surgical about where errors occur, we can make automated theorem proving dramatically more efficient. It’s a mindset shift from “start over” to “fix the smallest broken piece.”

Tom: And the numbers back it up. Eleven out of twelve Putnam problems, four out of five IMO problems, and at a fraction of the cost and time of previous systems. That’s not incremental progress, that’s a leap.

Jane: It really is. And the fact that the approach works with different underlying language models means it’s not tied to one specific piece of technology. As models get better, Mechanic will get better too.

Tom: So what’s the long-term impact here? I mean, we’re talking about AI that can prove math problems that stump most humans.

Jane: The long-term impact is that we’re getting closer to AI that can do genuine mathematical research. Not just checking proofs, but discovering new ones. The authors even mention that systems like DeepMind’s Aletheia are already moving toward research-level problems. Mechanic is another step in that direction.

Tom: And that could change how we do science, how we verify software, how we teach math. The possibilities are pretty wild.

Jane: They are. But for now, we should say goodbye to this paper. It’s been a fascinating look at how a clever workflow can squeeze so much more out of existing AI models.

Tom: Absolutely. Thanks to everyone who tuned in. Next up, we’ve got a paper on something completely different, so stay tuned.

Jane: See you all next time.

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

Academy of Mathematics and Systems Science, Chinese Academy of Sciences · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · School of Mathematical Science, University of Chinese Academy of Sciences

cs.CL

Submitted: 2026-08-16

Updated: 2026-08-18

Code: https://github.com/oOo0oOo/lean-lsp-mcp

License: http://creativecommons.org/licenses/by/4.0/

Importance score: 69/100

The gist: "For problems requiring complex mathematical reasoning, current systems rarely succeed on the first try and must repeatedly modify their proof strategies.

Key concepts

Sorrifier
The Sorrifier is a tool used within the Lean proof assistant. It acts as a placeholder for parts of an unfinished proof that are unknown, allowing the rest of the proof to be checked even when it's incomplete.
Formal Decomposition Workflow
This is how Mechanic operates. It takes an informal math sketch, translates it into formal code (Lean), and then breaks down any errors into smaller subgoals. It solves these subgoals independently and stitches them back together to complete the the overall proof.
Automated Theorem Proving
This is the process of using AI systems to prove complex mathematical statements. The paper describes a new approach that makes this process much faster and more efficient than previous methods, allowing it to tackle extremely difficult problems.

Terminology

Summary

Summary

The paper introduces Mechanic, a novel agent system for automated theorem proving that employs a sorry-driven formal decomposition strategy. The core problem addressed is the inefficiency of existing LLM-based theorem-proving agents when handling failed proof attempts. The authors state: "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 resolve this dilemma, Mechanic leverages the sorry placeholder in the Lean theorem prover. The key innovation is the Sorrifier, a module that "repeatedly substitutes incorrect proof blocks with sorry placeholders, continuing this process until the full proof successfully compiles in Lean. This process transforms a faulty proof into a sorried proof—a syntactically valid but incomplete proof. The algorithm is designed to handle cascading errors in dependent type systems by surgically targeting the innermost reported error and immediately recompiling after each modification to remove downstream errors. The final output is a structurally valid Lean proof containing a few sorry placeholders."

The overall workflow consists of four main steps, imitating human expert behavior:

  1. Informal Prove: A Reasoner LLM generates an informal proof sketch, which is iteratively refined through a feedback loop with a Verifier LLM. Each candidate solution is independently evaluated three times and accepted only if all three pass.

  2. Formal Prove: A Prover LLM translates the informal sketch into a Lean proof. Errors from the Lean compiler are processed, with unknown identifier errors routed to search tools (LeanDex, Loogle) and other errors analyzed by the Verifier for high-level strategy comments. This process runs for a predefined number of rounds.

  3. Subgoal Split: This involves three sub-steps:

  • Sorrify: The Sorrifier isolates and replaces erroneous components with sorry.

  • Extract: Each sorry location's tactic state and proof goal are extracted. The Reasoner identifies relevant hypotheses and formulates a self-contained subgoal. These subgoals undergo two-stage evaluation by the Verifier: syntactic verification via Lean and semantic evaluation for correctness and logical soundness.

  • Assemble: Once a subgoal is proven, it is reintegrated into the original proof by replacing the sorry with an apply tactic.

  1. Subgoal Process: Each extracted subgoal is processed recursively through the same pipeline. A termination mechanism prevents infinite recursion: if a subgoal yields a nested subgoal identical to itself, the system reverts to formal proving attempts, and after a threshold, the subgoal is deemed unprovable.

The paper's experiments evaluate Mechanic on 12 problems from the 2025 Putnam Mathematical Competition and 4 problems from the 2025 IMO (excluding the geometry problem P2). The primary model used is Gemini-3.1-Pro-Preview, with a knowledge cutoff of January 2025 to avoid data leakage. Baselines include Hilbert, Aristotle, Axiom, Seed-Prover 1.5, and Numina-Lean-Agent.

Main Results:

  • Putnam 2025: Mechanic solved 11 of 12 problems within budget, failing only on A5. It achieved optimal performance in both runtime and API cost, requiring only 114 minutes and 18.5 on average. Compared to baselines on the 11 solved problems, it showed advantages in time (5/11), cost, proof length (5/11), and theorem count (7/11).

  • IMO 2025: Mechanic solved all four tested problems. While slower on the simplest problem (P5), it showed a significant efficiency advantage as the difficulty of the problem increases. On the hardest problem (P1), its running time was roughly one-third of Seed’s. Analysis of proof trees showed Mechanic's trees are wide but shallow, whereas others are relatively deep, which contributes to efficiency since same-level proofs can be parallelized.

Ablation Studies:

  • Informal prove: Removing the informal proof step increased costs and lemma counts on harder problems (e.g., A2 became unsolvable, A3 cost rose from 19.51 to 23.31, A4 from 10.50 to 20.47). The authors conclude that a well-structured informal proof significantly reduces errors in formal proofs.

  • Different Models: Testing with Gemini 3.1 Pro, Claude 4.5 Opus, Deepseek 3.2 Reasoner, Seed 2.0 Pro, and Kimi K2.5 showed that only Gemini and Claude could solve all four test problems. The other models solved only one problem each, but this reflects a substantial improvement over the original model, where no problems could be solved.

The paper concludes that Mechanic achieves significant improvements in proving efficiency, highlighting the effectiveness of formal decomposition over traditional informal approaches. The authors note limitations, including the fixed pipeline structure, and propose future work to modularize the sorrifier as a standalone component integrated into the code agent to allow the model to autonomously invoke it as needed.

Improvements for AI systems

Based on the paper, here are the specific improvements I can implement in an AI system, along with what the improved system can do.

What I will build: A dedicated software module that acts as an intelligent error-triage system for Lean proofs. It will:

  • Parse Lean compiler error messages and identify the innermost failing block (e.g., a have or calc block).

  • Replace only that failing block with the sorry placeholder, leaving all surrounding correct code intact.

  • Recompile immediately after each single modification to eliminate cascading errors.

  • Repeat this process iteratively until the proof compiles (with sorry placeholders) or a maximum iteration count is reached.

What the improved AI system can do:

  • Instead of discarding an entire failed proof and regenerating from scratch, it will salvage 80–90% of the correct proof structure.

  • It will reduce the context length that the LLM must attend to during repair, because it isolates the error to a single, small subgoal rather than showing the model hundreds of lines of error messages.

  • It will avoid the context bloat problem that plagues iterative repair approaches, since each repair cycle only deals with a minimal, self-contained snippet.

This module will:

  • Dynamically adjust the number of informal proof iterations based on problem difficulty (e.g., fewer iterations for simple problems).

  • Decide whether to parallelize subgoal solving based on the proof tree structure (wide trees are parallelized, deep trees are processed sequentially).

  • Terminate a proof attempt early if the cost exceeds a user-defined budget (e.g., 100 per problem).

The improved system will be a self-optimizing formal theorem prover that:

  • Preserves correct proof structure during error recovery (via the Sorrifier).

  • Decomposes complex proofs into small, parallelizable subgoals (via extraction and reassembly).

  • Avoids infinite loops and dead ends (via semantic verification and depth limits).

  • Uses informal reasoning strategically (only for hard problems, with rigorous verification).

  • Adapts its strategy in real-time based on cost, time, and error type.

  • Achieves state-of-the-art efficiency: solving 11/12 Putnam 2025 problems at 1/3 the time and 1/5 the cost of the best baseline, with shorter proofs and fewer auxiliary lemmas.

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.

Sources

Related papers