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

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 $\mathbf{\text{TheoremForge}}$, a cost-effective formal data synthesis pipeline that decomposes the formalization process into five sub-tasks, which are $\mathit{\text{statement}}\mathit{\text{formalization}}$, $\mathit{\text{proof}}\mathit{\text{generation}}$, $\mathit{\text{premise}}\mathit{\text{selection}}$, $\mathit{\text{proof}}\mathit{\text{correction}}$ and $\mathit{\text{proof}}\mathit{\text{sketching}}$. By implementing a $\mathit{\text{Decoupled}}\mathit{\text{Extraction}}\mathit{\text{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 $\mathbf{\text{\$0.481}}$ per successful trajectory using Gemini-3-Flash. Crucially, our strategy increases data yield by $\mathbf{\text{1.6}}\times$ 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 \href{https://github.com/timechess/TheoremForge}{here}.