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

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked numbers in Tables 1 to 3, 5 to 12 and the in-text figures, Algorithm 1 steps, Sections 3.1 to 3.2.4, Appendices B to E and the prompts, and quotations; changed: technique 2 evidence pointed to an unrelated technique and now cites the paper’s own attribution to isolation, one comparison (hard mode against comment module) was wrong on A1, the informal-stage credit for the four ProverBench errors was widened beyond p6 and p28, Table 9 exclusion rule reworded, Table 1 averages note corrected, one unsupported one run each removed; Verus forms are marked inference, and the claim that a Verus function with assume verifies silently has no support in the Verus sources and is unchecked.

source: Qiu, Cao, Liu, Guo, Gao, Zhi, Feng, arXiv:2603.24465v2 (16 Aug 2026), COLM 2026, 30 pages with appendices A to E. The prover is Lean 4 with Mathlib and the tasks are competition mathematics. No part of the paper is about Verus; each Verus form is an inference.

earlier note: the notes hold an abstract-only entry for this paper (record id mechmath-2026 in distributed_verification_db/topic_agents.md). The algorithm, prompts, numbers and failure tiers below are not in that entry.

the problem it addresses, what is measured, what stays trusted

A long LLM-written proof rarely compiles at once. The two usual responses both waste work, as the abstract says (p.1): “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.” Here the former is repairing in place and the latter is discarding and regenerating. MechMath’s answer: keep everything that compiles, cut out only the failing pieces with Lean’s sorry placeholder, turn each hole into a standalone lemma, prove it in a fresh context, and plug it back.

measured: problems solved, wall-clock minutes, API dollars, number of lemmas and proof lines, on Putnam 2025 (12 problems), IMO 2025 (4 problems), miniF2F-test (244) and a 40-problem number-theory subset of ProverBench (Section 4, p.7)
setup: Gemini 3.1 Pro in all three LLM roles; Kimina Lean server; LeanDex and Loogle for search; Lean v4.15.0 for miniF2F and v4.26.0 otherwise (Section 4, p.7)
trusted: the Lean compiler and kernel, and the formal statements. The prover prompt begins its rules with (Appendix C.4.4, p.21): “Do NOT modify the formal statement in any way.” The same prompt forbids sorry, admit and native decide in a final proof.
Inference: every LLM judgement in the pipeline (informal proof accepted, subgoal judged sound) is advisory; a wrong judgement costs time, not soundness, because the assembled proof is still compiled by Lean. The paper does not state who formalized the Putnam and IMO statements or how their fidelity was checked.

technique 1: the Sorrifier, one innermost error at a time

what it is: a deterministic loop that turns a non-compiling proof into a compiling one with holes, by replacing the smallest block around the first error with sorry, recompiling, and repeating.

when to use: a proof still fails after a few repair rounds and most of its structure is believed sound.

why one error at a time (Section 3.1, p.4): “If all reported errors were processed simultaneously, it would lead to unnecessary deletion of valid proof segments.” A broken step corrupts the context for everything after it, so later errors are often not real.

steps, from Algorithm 1 (Appendix C.2, p.18), for i = 1 to N

remove redundant statements located after an existing sorry
compile; if valid (allowing sorry), return the code with success
if there are no errors or the compiler times out, return failure
select the primary error and take its line and column
find all structural blocks (such as have, calc) that contain that line
choose the innermost, defined as the shortest such block
if there is none, the error is outside any block: truncate the statement at the error position and append sorry
if the block is a calc or choose, replace the whole block with sorry
otherwise (have or replace), replace only the proof body with sorry, keeping the stated claim
if the code did not change, return failure; else loop

The main text gives the same two cases in prose (Section 3.1, p.4): “If the error lies within a have block, it replaces only the innermost failing proof with sorry.” and “If the error occurs elsewhere, the proof is truncated exactly at the erroneous line, and sorry is appended to close the state.” And the reason for step 2 on every pass: “Crucially, after a single modification is made, the Lean environment is immediately recompiled, instantly removing any downstream cascading errors tied to the previously broken context.”

the paper’s example (Figure 3, p.6): in theorem eq_trans (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c, the block have step2 : b = c := by exact h1 fails with a type mismatch; the Sorrifier rewrites it to have step2 : b = c := by sorry and leaves step1, step3 and the final exact step3 untouched.

Verus form. Inference: the placeholder is assume(P) for a claim and admit() or assume(false) for a body. The loop becomes:

run Verus on the function; take the first reported error
failing assert(P): replace with assume(P) (the claim is kept, its justification is dropped, as in step 9)
failing assert(P) by { ... }: keep P, replace the statement with assume(P)
failing body of a helper proof fn: replace the body with admit()
failing ensures at function end, or a failing precondition of a call: insert assume(false) just before that point, the analogue of truncate-and-append in step 7
failing invariant at loop end: add assume(I) as the last statement of the loop body; failing on entry: assume(I) before the loop
re-run Verus after each single replacement; stop when it verifies or when a replacement changes nothing

What changes: Lean blocks nest syntactically, so innermost means shortest; in Verus the unit is the single obligation Verus names. What does not carry over: sorry is visibly incomplete to Lean, which prints a warning, whereas a Verus function with assume verifies silently, so the final acceptance test must reject any remaining assume or admit. Whether Verus’s later errors are artefacts of an earlier one, as in Lean, the paper cannot say.

evidence

lines kept (Appendix E.1, p.28): “Empirically, across 104 successful invocations on miniF2F and 135 on ProverBench, the mechanism achieved an average reuse rate of 74.5% and 71.1% of the original proof skeleton lines, respectively, with individual case reuse rates spanning from 5% to 98%.”
ablation on Putnam 2025 A1 to A4, budget 128 LLM calls (Table 3(d), p.9, and Section 4.2, p.10): “As summarized in Table 3(d), the discard & retry strategy failed entirely (0/4), while the iterative repair strategy solved only three problems (3/4).” MechMath solved 4 of 4.
per problem, iterative repair against MechMath (Table 3(d)): A1 4 calls, 20 min, $1.59 a g ain s t 3, 18,$ 1.53; A2 failed against 31, 45, $4.89; A 342, 141,$ 16.30 against 69, 106, $11.60; A 4126, 518,$ 55.70 against 88, 114, $19.90 - Sorrifier invocations per solved problem average 12.6 on Putnam 2025 (Table 5, p.24; 11 problems) and 98.0 on IMO 2025 (Table 6, p.24; 4 problems) limits: on A3 MechMath used more LLM calls than repair (69 against 42). The ablation covers four problems; the paper reports no repeated runs. A reuse rate as low as 5% means the method sometimes keeps almost nothing. ## technique 2: turning each hole into a self-contained lemma what it is: at each `sorry`, read the prover's goal and hypotheses, let an LLM keep only the hypotheses that matter, and write a standalone lemma. steps (Section 3.2.3 “Extract”, p.5) 1. at each `sorry`, extract the tactic state and goal from Lean 2. the Reasoner decides which hypotheses and context conditions are relevant to the goal 3. the paper's rule: “Irrelevant hypotheses are discarded, and only those that are essential are retained.” 4. the Reasoner writes the lemma statement example (Figure 3, p.6): the state at the hole is `a b c : Nat`, `h1 : a = b`, `h2 : b = c`, `step1 : a = b`, goal `b = c`; the extracted lemma is `lemma eq_trans-0 (b c : Nat) (h2 : b = c) : b = c`, dropping `a`, `h1` and `step1`. Verus form. Inference: for each `assume(P)` left by technique 1, write `proof fn sub_k(params) requires R ensures P` whose body is to be found. Verus prints no hypothesis list at a program point, so the candidate facts for `R` must be gathered from the function's `requires`, enclosing `invariant` clauses, branch conditions on the path, and earlier `assert`s. The pruning step is the same. evidence: the paper credits its low cost to isolation of each failed subproblem (Appendix D.2, p.25): “MechMath extracts each failed subproblem into a clean, self-contained context and resolves it independently.” No ablation isolates the pruning of hypotheses. limits: pruning can drop a needed hypothesis; technique 3 exists to catch that. ## technique 3: checking a subgoal before spending effort on it, and routing by error type what it is: two checks on every extracted lemma, with a different reaction to each kind of failure. steps (Section 3.2.3, p.5-6; Appendix E.2, p.28; Appendix E.3, p.29) 1. syntactic: Lean checks that the lemma statement is well-formed 2. semantic, by the Verifier LLM, in two parts: extraction correctness (does the lemma reflect the step it came from) and logical soundness: “Logical soundness measures whether the subgoal can be proven, usually checked by whether there are obvious counterexamples or essential hypotheses missing.” 3. on a syntax or extraction error, return the subgoal to the Reasoner for re-extraction 4. on a logic error, do not try to prove the subgoal; send the diagnostic comment and the `sorry` location back to the parent proof for another round of error fixing (Appendix C.1, p.18) the paper's example (Appendix B.1, p.15-16; Putnam 2025 A2): a `calc` step needed (1/π)·y·(π − y) ≤ (2/π)·y on [0, π/2]. The Verifier substituted y = 0.5, got 0.421 on the left and 0.318 on the right, and flagged a logic error. The paper's conclusion: “This kind of subgoal should not be extracted.” Verus form. Inference: the syntactic check is Verus accepting the `proof fn` signature with body `admit()`. Extraction correctness can be checked mechanically, which the paper does by LLM: replace the `assume(P)` in the parent with a call to `sub_k` while its body is still `admit()`, and run Verus; if the parent verifies, the chosen `requires` hold at that point and the `ensures` suffices. That mechanical check is not in the paper. Logical soundness has no mechanical check in either system; an LLM searching for a counterexample, as here, or running the `requires` and `ensures` as executable tests on sample inputs, are the options. evidence (Table 12, p.29; share of generated subgoals with each error type): syntax 0.61% Putnam, 5.60% IMO, 0.41% miniF2F, 5.13% ProverBench; extraction 3.05%, 4.85%, 0.00%, 1.92%; logic 1.22%, 1.49%, 1.23%, 7.05%. The table gives no counts. On miniF2F (Appendix E.3, p.30): “Empirical statistics on the miniF2F benchmark further confirm the necessity of this module: across the evaluation, the Verifier successfully intercepts a logic error 5 times across 3 distinct problems and corrected an extract error once.” limits: the Verifier is an LLM; the paper reports no rate of false alarms or of unsound subgoals that passed. Appendix C.1 (p.18) calls the check a 3-stage “extract-assess” evaluation while Section 3.2.3 calls it two-stage. ## technique 4: plugging proved lemmas back in steps (Section 3.2.3 “Assemble”, p.6): “As illustrated in Step 3 of Figure 3, this reintegration is achieved by replacing each sorry placeholder with a corresponding apply tactic.” In Figure 3 `sorry` under `have step2 : b = c` becomes `apply eq_trans-0 …`. a real instance (Appendix B.2, p.16): the main theorem `imo_2025_p3` consists of `have step1 … step7` blocks, most closed by `exact imo_2025_p3_k …` with k from 0 to 8, each a separately proved lemma. Verus form. Inference: replace `assume(P)` with a call `sub_k(args);` inside a `proof { }` block, or with `assert(P) by { sub_k(args); }`. Verus then proves the lemma's `requires` at the call site, so a wrong extraction shows up here as a precondition failure. ## technique 5: recursion on subgoals with a no-progress stop steps (Section 3.2.4, p.6-7) 1. each subgoal goes through the whole pipeline again: informal proof, formal proof, repair, sorrify, extract 2. a subgoal that fails yields nested subgoals 3. no-progress test, in a sentence that the page break after p.6 splits: when a subgoal yields a nested “subgoal identical to itself, we deem the proof to have made no progress and revert to a formal proving attempt.” 4. cap: “If the number of such retries reaches a predefined threshold, the subgoal is considered unprovable, and the overall proving process terminates.” Without step 3 the loop need not end, since any failing proof can be sorrified down to its own statement. The threshold's value is not given. Verus form. Inference: unchanged. Identity of subgoals is equality of `requires` and `ensures` after normalising names. evidence on tree shape: Figure 4 (p.8) plots nodes per depth for IMO 2025 P4 and shows MechMath's tree as wide and shallow against Aristotle's and Seed's. Section 4.1 (p.8) draws the consequence that sibling proofs can run in parallel while parents wait for children. The figure's values are not given as numbers. ## technique 6: informal proof first, accepted only on three unanimous verdicts steps (Section 3.2.1, p.5; Appendix C.1, p.17-18; prompts C.4.1 to C.4.3, p.19-21) 1. the Reasoner writes an informal solution as numbered atomic steps, each with its justification, no Lean code, and none of the phrases “obviously”, “it is clear that”, “intuitively” 2. the Verifier scores it 1, 0.5 or 0 with a written evaluation 3. acceptance rule: “To improve the reliability of verification, each candidate solution is independently evaluated three times by the Verifier and is accepted only if all three evaluations judge it correct.” 4. otherwise the Reasoner revises, deciding for each feedback item whether it is valid or an evaluator error 5. at most 16 refinement iterations 6. a fast direct proving attempt precedes all this, for easy theorems (Section 4.2, p.10) Verus form. Inference: the informal proof corresponds to a written proof plan for a function: which invariant each loop keeps, which lemma each postcondition needs. Three independent reviews with a unanimity rule apply to any LLM-judged artefact, including a generated specification. evidence (Table 3(b), p.9; Putnam A1 to A4; cost in dollars and proof-tree nodes): with informal proof$ 4.21 / 1, $29.0/20,$ 19.5 / 9, $10.5/10; w i t h o u t i t$ 3.90 / 2, failed, $23.3/11,$ 20.5 / 44. So the informal stage cost more on A1 and was required for A2.

a side effect worth copying: on ProverBench MechMath identified four wrong benchmark statements (Section 4.1, p.9); Appendix D.3 (p.27) says p6 was flagged in the informal proof stage and the informal verifier rejected all attempts for p28, and does not say how p13 and p20 were found. It lists: p6 ignores a zero denominator; p13 omits d > 0 so negative divisors give negative remainders under Lean’s %; p20 uses natural numbers without a > 0, admitting a = 0, n = 0; p28 asserts remainder 4 where the true value is 2. Inference: asking for an informal proof of a formal statement, and treating repeated verifier rejection as a signal that the statement is wrong, is a cheap specification test.

technique 7: formalize by mirroring the informal steps, then a bounded number of repairs

steps (Section 3.2.2, p.5; Appendix C.1, p.18; prompts C.4.5 and C.4.6, p.22-23)

the Prover translates the informal solution step for step, each informal step becoming a have or calc block; the prompt says: “You MUST completely trust that the Informal Solution represents the most streamlined proof.”
one theorem per code block, no new lemmas or definitions, no single library lemma that proves everything
on errors, feed Lean’s messages back and ask for a fix that keeps the structure
bound: “For the formal proving, we perform an initial formalization attempt, followed by up to 4 rounds of error correction based on Lean’s compiler feedback.”
then hand over to technique 1

The reason for the bound (Section 3.2.2, p.5): “Therefore, it is unrealistic to expect that a continuously running fix–verify cycle will eventually correct all errors in the proof.”

Verus form. Inference: write the proof as a sequence of named intermediate asserts, one per plan step, so that technique 1 has small units to cut. A proof with few intermediate assertions gives the Sorrifier nothing to preserve; this dependence on proof style is my reading, not a claim of the paper.

technique 8: two optional helpers for hard problems (hard mode)

what it is (Section 4, p.8): a search module and a comment module added to the repair step.

search: “First, a retriever-based tool addresses syntax-level errors, such as unknown identifiers resulting from misspellings or version-induced library shifts, by providing the model with semantically relevant Mathlib documentation.”
comment: the Reasoner reviews the failing proof’s strategy and structure for the Prover, for tactic failures; the reviewer prompt (Appendix C.4.7, p.23) asks for dead ends, a better strategy, structural flaws, and snippets of 5 to 10 lines

Verus form. Inference: search corresponds to looking up vstd lemma names and signatures when Verus reports an unknown identifier; the comment module is a second model reading the failing proof without the error-fixing history.

evidence (Table 3(a), p.9; cost in dollars on A1, A2, A3, A4): easy 1.53, 4.89, 11.6, 19.9; plus search 3.28, 13.3, 11.1, 13.7; plus comment 6.33, 5.70, 6.19, 6.42; both 4.21, 29.0, 19.5, 10.5. Putnam B1 and B6 were solved only in hard mode (Table 1, p.7).

limits: both together cost more than easy mode on three of the four problems, and more than the comment module alone on three of the four (A1: 4.21 against 6.33).

technique 9: three failure tiers that decide between local repair and regeneration

what it is (Appendix E.3, p.29): a classification of a failing proof.

F1, leaf-step failure: the scaffold and intermediate claims are sound and one tactic fails. Sorrify and extract.
F2, false intermediate claim: a have is mathematically false. The subgoal check raises a logic error and the parent proof is regenerated with that hint.
F3, skeleton defect: wrong induction variable, wrong hypothesis, wrong case split. Of this tier the paper says: “Because these defects disrupt the core mathematical architecture and sit entirely beyond the scope of the Sorrifier’s local processing, addressing F3 flaws relies exclusively on the upstream module executing a thorough global skeleton reconstruction.”

the paper’s case (Appendix E.3, p.30; ProverBench number theory p31): strong induction directly on n could not supply the hypothesis for n.minFac (F3); the proof was regenerated with a strengthened statement ∀ n m, m ≤ n → … and induction on n; the one remaining failure, 0 < b, was sorrified as a leaf (F1).

Verus form. Inference: F1 is a failing assert whose claim is true; F2 is an assert or invariant that is false; F3 is a wrong loop invariant shape, a wrong decreases measure or a wrong lemma statement to induct on. F2 and F3 call for rewriting, and applying technique 1 to them yields unprovable lemmas.

limits: the paper does not describe a classifier that assigns a tier in advance; the tier becomes known through the subgoal check or through repeated failure.

results across benchmarks

Putnam 2025 (Table 1, p.7): easy mode solves 9 of 12, hard mode 11 of 12; A5 unsolved by both. Single models at Pass@32 (Goedel Prover V2 32B, Gemini 3.1 Pro, Claude 4.5 Opus) solve 0 of 12. Hilbert with the same Gemini model solves 1 (B3). Averages over each system’s own solved problems (Axiom and Numina exclude A5, Table 1 caption): easy 67.2 min, $9.99, 11 l e mma s; ha r d 114 min,$ 18.5, 14 lemmas; Numina 165 min, $72.7, 17 l e mma s; A x i o m 187 min, 36 l e mma s; S ee d 196 min, 49 l e mma s . S ee d, A x i o man d N u mina f i g u r es a r e t ak e n f r o m t h e i r o w n r e p or t s (S ec t i o n 4, p .8) . - I M O 2025, p r o b l e m s P 1, P 3, P 4, P 5, ha r d m o d e (T ab l e 2, p .8) : 363, 137, 178, 110 min, a v er a g e 197; N u minaa v er a g e 273; S ee d a v er a g e 458; cos t$ 141, $43,$ 95, $47, a v er a g e$ 82.
miniF2F-test: 242 of 244 (99.2%), at most 512 LLM calls per problem and 57.6 on average over the problems left after excluding those the Prover solved directly in one turn (Section 4.1, p.9; Appendix D.2, p.24; Table 9, p.26). By category (Table 11, p.28): IMO 19/20, Number Theory 67/68, the rest complete.
ProverBench number theory subset: 24 of 40 against Hilbert’s 16 of 40 (Appendix D.3, p.26-27), average 45.2 calls and $2.97 per solved problem (Table 10, p.27). ## contradictions and numbers that do not add up - Table 3's caption (p.9) says: “(b), (c) and (d) is conducted on MechMath-Hard, since the easy mode fails in most of these settings.” The MechMath rows of (d), time 18, 45, 106, 114 and cost 1.53, 4.89, 11.60, 19.90, are the easy-mode figures of Table 1. - A5 budget: Section 4.1 (p.8) says “Although MechMath does not solve A5 within the$ 100 limit, the performance profiles of Axiom and Numina confirm the high computational demands of this problem.” Appendix C.1 (p.17) says “We assign a budget of $100 f or P u t nam 2025 an d$ 200 for IMO, except $300 f or P u t nam 2025 A 5, w hi c hi s w i d e l y r eco g ni z e df or i t s d i f f i c u l t y d u e t o t h e ab se n ceo f esse n t ia l t h eor e m s .” - S ec t i o n 4.2 (p .10) s a y sse a r c han d co mm e n t m o d u l esr e d u ce d cos t an d l e mma co u n t o n A 3 an d A 4. T ab l e 3 (a) s h o w s t ha t f or A 4 o n l y; o n A 3 ha r d m o d ecos t s$ 19.5 against 10 to $82 per hard problem with a general frontier model, no fine-tuning, show that such a loop needs no proprietary model.

techniques for the catalog

innermost-error sorrifying — replace the smallest block around the first compiler error with a placeholder, recompile, repeat until the proof compiles with holes
truncate-and-close — when an error is outside any structured block, cut the proof at that position and close the goal with a placeholder
hole-to-lemma extraction — read goal and hypotheses at each placeholder, keep only relevant hypotheses, and emit a standalone lemma
two-stage subgoal check — compile the lemma statement, then have an LLM test extraction fidelity and search for counterexamples before any proof attempt
error-type routing — re-extract on syntax or extraction errors, send logic errors back to the parent proof for repair
apply-back assembly — replace each placeholder with an application of its proved lemma
no-progress termination — stop recursing when a subgoal reproduces itself, retry directly, and give up after a fixed number of retries
unanimous triple verification — accept an LLM-judged artefact only when three independent evaluations all pass it
step-mirrored formalization — make each numbered informal step one named intermediate claim so failures stay local
bounded repair before decomposition — allow a fixed small number of whole-proof repair rounds, then switch to cutting
search-and-comment repair aids — add library lookup for unknown identifiers and a strategy review by a second model on hard problems
F1/F2/F3 failure tiers — treat true-claim leaf failures locally, false intermediate claims by regenerating the parent, skeleton defects by regenerating the plan
informal-proof specification test — treat persistent verifier rejection of every informal proof as evidence that the formal statement is wrong

Last edited: 2026-10-13

Keyboard shortcuts

Steven Hé (Sīchàng)