{"id":"arxiv/2609.34960","url":"https://arxiv.org/abs/2609.34960","tags":["cs.AI","math.OC"],"score":0,"title":"ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization","domain":"cs.AI","source":"arxiv","authors":["Feiming Wang","Daibo Li","Kun Yuan"],"reviews":0,"subject":"cs.AI","summary":"Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction. Given a published algorithm, target theorem, and source proof, ProofLoom autonomously constructs the Lean model and supporting theory. Open proof obligations drive the development of definitions, interfaces, lemmas, and proof plans. Signature…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-28","reactions":{}}