ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
cs.AI, math.OC
Submitted: 2026-09-28
Updated: 2026-09-28
Code: https://github.com/Trace231/ProofLoom
Sources
- Faithful Autoformalization via Roundtrip Verification and Repair
- A formally verified proof of the Central Limit Theorem
- ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization
- Momentum-Based Variance Reduction in Non-Convex SGD
- A Lean 4 Formalization of Scott's \emph{Continuous Lattices} (1972)
- SPIDER: Near-Optimal Non-Convex Optimization via Stochastic Path Integrated Differential Estimator
- Sharpness-Aware Minimization for Efficiently Improving Generalization
- LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving
- Convergence Analysis of the Lion Optimizer in Centralized and Distributed Settings
- Automated Conjecture Resolution with Formal Verification
- Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
- Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimization
- PAGE: A Simple and Optimal Probabilistic Gradient Estimator for Nonconvex Optimization
- Decentralized Optimization over Time-Varying Row-Stochastic Digraphs
- G-Eval: NLG Evaluation using GPT-4 with Better Human Alignment
- The Faithfulness Gap: Certifying Semantic Equivalence Between Natural-Language and Formal Mathematical Statements
- miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward
- (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
- CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
- An enhanced Baillon-Haddad theorem for convex functions on convex sets
Related papers
- MAVEN-T: Reinforced Heterogeneous Distillation for Real-Time Multi-Agent Trajectory Prediction
- Model Discovery Agent: LLM-assisted Bayesian experiment design for data-efficient discovery of mechanistic world models
- Agents' Last Exam
- The Clinician's Veto: Navigating Trust, Liability, and Uncertainty in Autonomous AI Prescribing
- MindHelper: Closed-Loop Embodied Mental-State Reasoning for Precision Intervention
- Incumbent Advantage: Brand Bias and Cognitive Manipulation Dynamics in LLM Recommendation Systems