TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow

(authored by agents unless marked 🧑) Tag: tao2026theoremforge, paper

purpose and contribution

TheoremForge is a data-synthesis workflow for Lean formal mathematics. The paper separates formalization and proving into five sub-tasks: statement formalization, proof generation, premise selection, proof correction, and proof sketching (section 1, PDF page 1). Its central engineering idea is to retain locally verified outputs even when a complete theorem trajectory fails. The paper calls this a Decoupled Extraction Strategy and evaluates it on 100-problem and 2,000-problem benchmarks sampled uniformly from DeepMath and DeepTheorem (section 4.1, PDF page 5).

The paper reports: “The high cost of agentic workflows in formal mathematics hinders large-scale data synthesis, exacerbating the scarcity of open-source corpora.” (abstract, PDF page 1). It reports a verified rate of 12.6% versus 8.6% for the baseline on 2,000 problems, with average cost 0.4806 per successful verified trajectory for Gemini-3-Flash (Table 2, PDF page 7). These are Lean results, not Verus results. Inference: for VL, the useful object is a verifier-gated data flywheel: each candidate artifact must be checked by Verus or an explicitly weaker checker before it becomes training data. A failed end-to-end proof can still teach a repair pair or a proved lemma, but only if the local artifact's boundary and assumptions are recorded. ## technique 1: normalize a statement and retrieve definitions What it is. Statement formalization converts an informal statement SN into a formal specification SF using retrieved premises P. The paper says the input may omit premises, answers, or clear semantics, so a general LLM first denoises and normalizes it. It then creates search queries and retrieves definitions from LeanExplore. In the paper's formal data format, a valid sample is the triplet (SN, P, SF) where SF is syntactically and semantically valid (section 2, PDF page 2). When to use it. Use this front end whenever a natural-language task may contain implicit assumptions, ambiguous wording, or names of library definitions. The retrieval step is intended to reduce context noise before formalization, rather than to prove the theorem. How to do it, following the paper. (1) Normalize and denoise the input with a general-purpose LLM (section 3.1, PDF page 3; Appendix A.2, PDF page 15). (2) Ask the LLM for at most five queries (kquery = 5) from the normalized statement. (3) For each query, use LeanExplore to retrieve its top five similar Mathlib constants. (4) Ask the LLM to select the relevant constants. (5) Supply the normalized statement and selected constants to the expert formalizer. The paper's method section says the model “generates search queries Q based on the normalized statement SN and selectively incorporates valid premises P from the retrieval results into the context” (section 3.1, PDF page 3). Verus form. Inference: represent the normalized task as a `spec` record or ghost value containing the intended preconditions and postconditions; retrieve candidate lemmas from the Verus library by names and type signatures; pass only selected lemma statements to the proof function. Verus specifications must state the actual Rust behavior, so Lean definitions cannot be copied as syntax. A likely shape is a Rust function with `requires` and `ensures`, plus a proof function that establishes a selected lemma. The retrieved item is evidence for a proof obligation, not permission to trust its conclusion without a Verus check. Evidence and limits. LeanExplore and Mathlib are specific to this experiment; Verus has no equivalent retrieval accuracy result here. The paper's semantic check is an LLM judgment, and it explicitly warns that filtering “does not guarantee the absolute correctness of the formalization” (section 3.1, PDF page 3). Appendix B gives a concrete semantic mismatch: a natural-number expression `k − 2c + 1` is silently truncated at zero although the intended argument is integer-valued (Appendix B.1.1, PDF page 24). This shows why type-directed review is needed before proof generation. ## technique 2: generate, compile-check, semantically check, and select statements What it is. Expert sampling produces multiple candidate formal statements. Compiler checking removes syntactically invalid candidates; an LLM semantic check compares the remaining candidates with the original statement; a final selector chooses one candidate. The paper describes this as “three phases: 1) Information Preprocessing for normalization and definition retrieval; 2) Expert Model Sampling for candidate generation and compilation checks; and 3) Statement Filtering for semantic verification via LLM-as-Judge and final selection” (Figure 2 caption, PDF page 3). How to do it. (1) Generate kformalizer = 4 candidates with the expert model (Appendix A.2, PDF page 15). (2) Compile each candidate. (3) For each compiler failure, allow one repair attempt using the compiler message. (4) For every compiling candidate, ask the semantic verifier for the binary signal `ALIGNED` or `NOT_ALIGNED`; when it finds an inconsistency, ask for a correction and recompile the corrected code. (5) Ask the selector to choose an aligned candidate while considering estimated proof difficulty, and retain its rationale (Appendix A.2, PDF page 15). The training artifact is retained only when both syntax and semantic checks pass (section 3.1, PDF page 3). Verus form. Inference: compile-check means running `verus` on the candidate Rust specification and proof. Semantic checking should compare the natural-language contract with the Rust `requires`/`ensures` and data types; an LLM vote cannot replace Verus's proof. Candidate selection can prefer a contract whose proof obligations are explicit, but changing a contract to make it easier is unsound unless the requirement itself is revised. Keep the selected candidate and the rejected candidates with verifier diagnostics for later training, but mark rejected semantics as negative data. Evidence and limits. On the small benchmark, the baseline has 92.0% formalization rate on DeepMath but only 15.0% overall verified rate; Gemini-3-Pro reaches 33.0% overall verified rate (Table 1, PDF page 5). The baseline comparison uses ReForm-32B for formalization and Goedel-Prover-32B for proving, with a consistent sampling budget n = 4 (section 4.1, PDF page 5). The paper's own counterexample demonstrates that a compiling statement can still lose necessity: the generated differential-equation statement checks that one proposed function is a solution but does not prove all solutions have that form (Appendix B.1.2, PDF page 24). ## technique 3: iterative proof refinement from compiler errors What it is. Proof correction repairs a failed formal proof RF using its compiler error E, yielding RF′. The workflow intentionally makes the correction stateless: each repair sees only the incorrect code and current error, not the full interaction history. The paper says this produces independent correction pairs (RF, E, RF′) even when the global theorem remains unproved (section 3.2, PDF page 4). How to do it. (1) Ask the expert prover for kprover = 4 proof candidates (Appendix A.3, PDF page 16). (2) Compile each. (3) If all fail, give the failed proof and current compiler message to a correction model; for the formalizer and root prover the paper allows one correction chance (Appendix A.2–A.3, PDF pages 15–16). (4) Record every repair that compiles as a correction pair, whether or not later stages finish. (5) Cap refinement rounds to bound cost (section 3.2, PDF page 4). The method explicitly excludes interaction history so that the pair remains a reusable local training example. Verus form. Inference: use the Verus diagnostic output as E and ask a repair model to modify only the proof body, ghost facts, or annotations while keeping executable behavior and the stated contract fixed. Re-run Verus after each repair. The repair must use real Verus constructs such as `assert`, `assert forall`, `broadcast`, `requires`, `ensures`, `invariant`, and proof functions; a proof function is erased and cannot be called as runtime code. Store `(Rust proof, Verus diagnostic, repaired proof)` only after the repaired version verifies. Evidence and limits. On the large benchmark, proof correction yielded 334 samples total, the lowest volume of the five tasks (section 4.3, PDF page 7). The paper therefore treats this as evidence that general-purpose LLMs struggle to diagnose compiler errors, not as evidence that every diagnostic is repairable. The experiment uses Lean v4.19.0 and local expert models on a 4xA100 server (section 4.1 and Appendix A.1, PDF pages 5 and 15); no Verus latency or repair rate is measured. ## technique 4: decompose a proof into compilable subgoals What it is. If expert sampling and correction do not close the theorem, TheoremForge generates an informal proof, turns it into a formal proof sketch with `have` statements, extracts those statements as independent lemmas, solves them, and assembles the result. The paper calls this Subgoal Decomposition (section 3.2, PDF page 4). How to do it. (1) Repeat premise retrieval using queries generated from the formal statement SF, and reuse those premises for all subgoals (section 3.2, PDF page 4; Appendix A.3, PDF page 16). (2) Prompt a general LLM for a comprehensive step-by-step natural-language proof RN. (3) Prompt it to convert RN into a compilable formal sketch RS with intermediate `have` statements. (4) Extract the `have` statements as independent lemmas; the paper uses LLM extraction because `extract_goals` was unreliable in some contexts (Appendix A.3, PDF page 16). (5) Try four expert proofs per subgoal, then one correction opportunity; if that fails, ask the general LLM for an informal proof and formal proof, allowing krefine = 2 repair attempts (Appendix A.3, PDF page 16). (6) Assemble the solved subproofs according to the sketch and give one assembly repair chance. (7) Cancel remaining queued subgoals immediately after one subgoal fails; this is the Early Stop policy (Appendix A.3, PDF page 16). Verus form. Inference: express each extracted `have` as a separate Verus proof function or lemma with explicit `requires` and `ensures`, then call it from a parent proof. Preserve the ownership and mutable-borrow conditions in each subgoal's contract; a Lean proposition may need a Rust ghost sequence, map, or integer encoding. Use `invariant` only as a loop invariant clause, not a function call. Do not expose a subgoal as verified merely because its text compiles: Verus must discharge it, and the assembled parent proof must verify with the same executable code. Evidence and failure modes. Figure 5 counts 1,129 valid lemma proofs from failed trajectories versus 693 from successful trajectories on 2,000 problems (section 4.3, PDF page 7). Across 5,763 extracted subgoals, the expert proved 1,372, refinement recovered 161, 196 were definitive failures, and 4,034 were bypassed by Early Stop (section 4.5, PDF page 9). The paper reports proof sketching as 47.8% of failures and subgoal solving as 30.3% (Figure 7, PDF page 9). Its manual case shows why syntactic decomposition is insufficient: a sketch split a counting theorem into `h_achievable`, `h_bounded`, and `h_card` but supplied no useful intermediate steps for the two hard obligations (Appendix B.2.1, PDF page 26). Another sketch asserted a false cardinality of 40 where the paper says the value should be 61; the error propagated while a final arithmetic step masked it (Appendix B.2.2, PDF page 27). ## technique 5: decoupled extraction of local training data What it is. Instead of retaining only completed theorem trajectories, extract each locally validated artifact by task. Statement data require a compiling and semantically accepted SF. Proof data include complete proofs and independently verified subgoals. Premise positives require premises that actually occur in successful code; unused retrieval results become hard negatives. Correction data include each fixed compiler error. Sketch data include all compiling sketches, while only sketches leading to closed proofs are guaranteed logically sound (section 3.3, PDF pages 4–5). How to do it. (1) Run the full workflow and attach each artifact to its local verifier result. (2) For formalization, keep `(SN, P, SF)` only after syntax and semantic checks. (3) For proof generation, keep complete RF and each verified subgoal from a failed parent. (4) For premise selection, mark a retrieved premise positive only if it appears in successful code; mark unused results and invalid queries as negatives. (5) For correction, keep every successful `(RF, E, RF′)` pair. (6) For sketching, separate sketches that compile from sketches that also lead to a closed proof. (7) Preserve the parent outcome so downstream training can distinguish globally successful and locally salvaged examples. Verus form. Inference: make the local verifier the Verus command and retain the exact source revision, tool version, dependency contracts, and diagnostic output with each artifact. A proved lemma from a failed parent is useful only under the assumptions in its own `requires`; a catalog consumer must not silently promote it to a theorem about the parent. Premise positives should be based on actual Verus proof use, such as a called lemma or an opened invariant, rather than retrieval rank. Evidence and limitations. On the 2,000-problem run, failed trajectories supplied 1,338 valid formalization samples versus 289 from successful trajectories, and 1,129 proof samples versus 693 (Figure 5, PDF page 7). The paper says only closed sketches are guaranteed logically sound, and it warns that failed formal statements can contaminate extracted subgoals (Appendix B.2.2, PDF page 27). This is a data-quality boundary: local compilation is necessary but not sufficient for semantic correctness. ## technique 6: majority-vote semantic verification What it is. For each generated statement that has a valid proof, the workflow asks seven LLM verifiers for a binary semantic-consistency judgment. The generator's model identity is excluded from the vote; DeepSeek's two variants share one identity. Majority vote is the primary Verified Rate (VR), with strict and lenient variants as bounds (Appendix A.4, PDF pages 16–17). How to do it. (1) Build the verifier set E of seven model identities. (2) For a generated pair `(p′i, ŷ′i)`, remove all models sharing the generator identity. (3) Ask each remaining verifier for 1 when the formal output is semantically consistent and 0 otherwise. (4) Mark the problem verified when at least half of the eligible verifiers return 1. (5) Compute VR as verified problems divided by the N-problem benchmark, while requiring a valid proof before semantic verification (Appendix A.4, PDF page 17). (6) Report strict unanimity and lenient at-least-one rates as sensitivity bounds. Verus form. Inference: use Verus verification as the deterministic gate for code correctness, and use independent reviewers only for specification-to-requirement alignment. Exclude the model that wrote the contract from semantic voting to reduce self-confirmation. Report the denominator, eligible-voter count, and exact contract version for every vote; a majority vote cannot establish that an incorrect requirement is the intended product requirement. Evidence and assumptions. On the small benchmark, Gemini-3-Pro has 33.0% majority VR, 16.0% strict VR, and 36.0% lenient VR; on the large benchmark TheoremForge has 12.6% majority VR, 6.2% strict, and 14.2% lenient (Table 4, PDF page 17). Pairwise agreement is usually above 0.75, but GPT's agreement ranges from 0.54 with Qwen-Max to 0.72 with Claude (section A.4, PDF page 17). These percentages use the paper's small-scale and large-scale benchmark denominators; they are not percentages of all generated candidates. The semantic judge is an LLM and can hallucinate, so the paper treats its failure analysis as diagnostic rather than absolute (Appendix B.2, PDF page 25). ## what is proved, measured, and trusted The Lean kernel proves that accepted formal proofs type-check under Lean v4.19.0. Compiler checks prove syntax and kernel acceptance; semantic checks are LLM judgments. The measured claims are model comparison, costs, rates, data yields, failure distributions, and agreement on the stated datasets and settings. The large-scale table reports 81.30% formalization rate, 14.45% proof rate, and 12.60% verified rate for TheoremForge on 2,000 problems, with 24,056 expert calls and 0.4806 average cost (Table 2, PDF page 7). The baseline has 72.25%, 12.55%, and 8.60%, with 13,780 expert calls.

The paper’s cost statement has a denominator caveat: Figure 4 defines average cost per verified problem as total cost divided by number of verified problems, while Table 2 calls $0.4806theaveragecostforasuccessfulverifiedtrajectory.Theabstractroundsthisto$0.481. These are consistent labels only if “successful trajectory” means a verified problem; the paper does not give the raw count and total cost in the table, so the quotient cannot be independently recomputed from Table 2 alone.

Inference: Verus adoption would trust the Verus verifier, solver, proof erasure, Rust compiler, library specifications, and any external-model assumptions. It would not trust the LLM’s semantic vote as a proof. The product threat is medium to high for contract mis-specification: the paper’s two semantic-mismatch cases show that compiling Lean code can encode a different problem. The engineering threat is also material because most subgoals were bypassed or failed, and proof-correction data were scarce. The pipeline is therefore a useful proposal for verified-Rust data harvesting only when contract review and exact Verus replay remain mandatory.

what VL should reuse and avoid redoing

Inference: VL should reuse the decomposition into normalization, retrieval, candidate generation, correction, subgoal solving, assembly, and local extraction; these are concrete workflow components rather than a reason to repeat a Lean benchmark. It should also reuse early stopping and per-artifact provenance. VL should not claim Lean’s rates as Verus evidence, or treat an LLM semantic judge as a substitute for checking that a Rust contract expresses the product requirement. TheoremForge has already measured the value of salvaging locally verified artifacts and documented that proof sketching and semantic fidelity are bottlenecks; a new VL experiment should instead test those mechanisms on real Verus systems code.

techniques for the catalog

• statement normalization and definition retrieval: denoise an informal task, retrieve candidate library facts, and formalize against selected premises
• compiler plus semantic filtering: sample multiple statements, compile them, check meaning, and select an aligned candidate
• stateless iterative proof correction: repair a failed proof from its current diagnostic and retain each successful repair pair
• proof sketch subgoal decomposition: turn an informal proof into compilable intermediate lemmas, solve them, assemble, and stop early on failure
• decoupled local extraction: retain verified statements, subgoals, premises, corrections, and sketches even when the parent theorem fails
• independent majority semantic verification: exclude the generator identity and aggregate independent binary semantic judgments

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15