ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization

Formalizing research-level stochastic optimization in Lean requires a Lean model of the algorithm and domain theory that connects foundational libraries to its convergence proof. Published proofs often compress these connections, and whether a Lean model supports the complete proof may become clear only as the proof proceeds. Revising the model to restore provability, however, can change the mathematical claim. We introduce ProofLoom, an LLM-agent autoformalization system for Proof-Obligation-Driven Theory Construction. Starting from a Lean algorithm model and its main theorem statement, ProofLoom uses open proof obligations to select definitions, interfaces, and lemmas to reuse or construct. Signature contracts record the published evidence and derived obligations for each revision of the Lean model, and an independent Judge rejects revisions that add unsupported assumptions or weaken the theorem. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows that argument. Certified developments contribute verified Lean code and natural-language construction records to SOptLib for reuse across algorithms. On fifteen textbook and research-paper tasks, ProofLoom obtains mean human ratings of 6.3/7 and 6.4/7, compared with 4.9/7 and 5.0/7 for the strongest of six baselines. Across 33 developments, it produces 490,693 lines of algorithm-local Lean code with no sorry. The formalizations also expose 28 incorrect formulas, proof gaps, and algorithm–analysis mismatches in published sources across 22 developments, each with checked evidence. Anonymous code and supplementary materials are available at https://anonymous.4open.science/r/ProofLoom-E71F/.