TheoremForge 用低预算 agentic pipeline 回收失败轨迹，建立 formal-math data flywheel

TheoremForge 将 formalization 拆成 statement formalization、proof generation、premise selection、proof correction 与 proof sketching 五个子任务，并提出 Decoupled Extraction Strategy，从整体失败的 agent trajectories 中回收仍然有效的局部训练信号。在 2,000 题实验上，paper-reported verified rate 从 8.6% 提升到 12.6%，使用 Gemini 3 Flash 时每条 successful trajectory 平均成本约 0.481 美元，proof-generation data yield 提升约 1.6×。