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

arXiv: https://arxiv.org/abs/2601.17332 · HTML: https://mlsanity.com/paper/2601.17332/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 29 of its 39 references that are in the map.
- First posted on arXiv 24 Jan 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)
- Synthetic data and self-improvement for LLMs / [Self-play RL for reasoning](https://mlsanity.com/synth/self-play-rl-for-reasoning/)

## Builds on (most cited first, 29 of 29)

- [AFlow: Automating Agentic Workflow Generation](https://mlsanity.com/paper/2410.10762/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepMath-103K: A Large-Scale, Challenging, Decontaminated, and Verifiable Mathematical Dataset for Advancing Reasoning](https://mlsanity.com/paper/2504.11456/) (2025)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Multi-agent Architecture Search via Agentic Supernet](https://mlsanity.com/paper/2502.04180/) (2025)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Agentic Reasoning and Tool Integration for LLMs via Reinforcement Learning](https://mlsanity.com/paper/2505.01441/) (2025)
- [TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts](https://mlsanity.com/paper/2407.03203/) (2024)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [EvoAgentX: An Automated Framework for Evolving Agentic Workflows](https://mlsanity.com/paper/2507.03616/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers](https://mlsanity.com/paper/2509.06493/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [DyFlow: Dynamic Workflow Framework for Agentic Reasoning](https://mlsanity.com/paper/2509.26062/) (2025)
- [QualityFlow: An Agentic Workflow for Program Synthesis Controlled by LLM Quality Checks](https://mlsanity.com/paper/2501.17167/) (2025)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization](https://mlsanity.com/paper/2510.24592/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [Adaptive Self-improvement LLM Agentic System for ML Library Development](https://mlsanity.com/paper/2502.02534/) (2025)
- [Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework](https://mlsanity.com/paper/2412.16953/) (2024)
- [Tree-of-Code: A Tree-Structured Exploring Framework for End-to-End Code Generation and Execution in Complex Task Handling](https://mlsanity.com/paper/2412.15305/) (2024)
- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [Collaborative Mean Estimation Among Heterogeneous Strategic Agents: Individual Rationality, Fairness, and Truthful Contribution](https://mlsanity.com/paper/2407.15881/) (2024)
- [RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation](https://mlsanity.com/paper/2505.22846/) (2025)
- [SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation](https://mlsanity.com/paper/2510.25975/) (2025)

## Built on by (most cited first, 1 of 1)

- [OProver: A Unified Framework for Agentic Formal Theorem Proving](https://mlsanity.com/paper/2605.17283/) (2026)

## Abstract (arXiv)

The high cost of agentic workflows in formal mathematics hinders large-scale data synthesis, exacerbating the scarcity of open-source corpora. To address this, we introduce TheoremForge, a cost-effective formal data synthesis pipeline that decomposes the formalization process into five sub-tasks, which are textitstatement formalization, textitproof generation, textitpremise selection, textitproof correction and textitproof sketching. By implementing a textitDecoupled Extraction Strategy, the workflow recovers valid training signals from globally failed trajectories, effectively utilizing wasted computation. Experiments on a 2,000-problem benchmark demonstrate that TheoremForge achieves a Verified Rate of 12.6%, surpassing the 8.6% baseline, at an average cost of only 0.481 per successful trajectory using Gemini-3-Flash. Crucially, our strategy increases data yield by 1.6× for proof generation compared to standard filtering. These results establish TheoremForge as a scalable framework for constructing a data flywheel to train future expert models. Our code is available hrefhttps://github.com/timechess/TheoremForgehere.