mlsanityData to 7 Oct 2026

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

arXiv 2609.34960 ↗First posted 28 Sep 2026cs.AI math.OCcited by 0

Not on the map. Why?

Abstract (arXiv)

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 contracts record evidence and obligations for model revisions; an independent Judge rejects unsupported assumptions and weakened conclusions. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows it. Across tasks, SOptLib accumulates verified mathematics and construction experience: reusable results are extracted, generalized, and verified, while modeling decisions and failed proof routes are recorded. Later tasks retrieve these results and records and contribute new developments, forming a cycle of construction, accumulation, and reuse. 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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 39 of its 53 references that are in the map. First posted on arXiv 28 Sep 2026.

Builds on

39 of 53 references.

References · 39

  1. 2023G-Eval: NLG Evaluation using GPT-4 with Better Human Alignmentcited by 2,205
  2. 2020Sharpness-Aware Minimization for Efficiently Improving Generalizationcited by 1,404
  3. 2019On the Convergence of Adam and Beyondcited by 834
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2019Momentum-Based Variance Reduction in Non-Convex SGDcited by 302
  7. 2018SPIDER: Near-Optimal Non-Convex Optimization via Stochastic Path Integrated Differential Estimatorcited by 283
  8. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  9. 2020PAGE: A Simple and Optimal Probabilistic Gradient Estimator for Nonconvex Optimizationcited by 116
  10. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  11. 2024MARS: Unleashing the Power of Variance Reduction for Training Large Modelscited by 59
  12. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
27 more
  1. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  2. 2026Automated Conjecture Resolution with Formal Verificationcited by 21
  3. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  4. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  5. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  6. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  7. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
  8. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  9. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  10. 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 12
  11. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 11
  12. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 7
  13. 2025Convergence Analysis of the Lion Optimizer in Centralized and Distributed Settingscited by 6
  14. 2025MASA: LLM-Driven Multi-Agent Systems for Autoformalizationcited by 6
  15. 2026Faithful Autoformalization via Roundtrip Verification and Repaircited by 6
  16. 2014A formally verified proof of the Central Limit Theoremcited by 5
  17. 2025Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approachcited by 5
  18. 2026Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoningcited by 4
  19. 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalizationcited by 4
  20. 2018On the Properties of Convex Functions over Open Setscited by 3
  21. 2026The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statementscited by 3
  22. 2022A simple proof of the Baillon-Haddad theorem on open subsets of Hilbert spacescited by 2
  23. 2026FormalRx: Rectify and eXamine Semantic Failures in Autoformalizationcited by 2
  24. 2019An enhanced Baillon-Haddad theorem for convex functions on convex setscited by 1
  25. 2025Decentralized Optimization over Time-Varying Row-Stochastic Digraphscited by 1
  26. 2026(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofscited by 1
  27. 2026A Lean 4 Formalization of Scott's Continuous Lattices (1972)cited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
  2. 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
  3. 2026Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
  4. 2026Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
  5. 2024ImProver: Agent-Based Automated Proof Optimization
  6. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?
  7. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
  8. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics