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

1 Introduction

• The challenge is that published proofs compress links between probability, analysis, and algorithms, while model mismatches may emerge only when a proof reaches a dependent step.For stochastic mirror descent, deriving a conditional expectation identity at a random iterate from a fixed-query oracle assumption requires a bridge lemma and a model specifying sampling dependencies.Source: §1 · pp. 1–2
• Mean human ratings were 6.3/7 on FOML and 6.4/7 on research-paper tasks, versus 4.9/7 and 5.0/7 for the strongest baseline.ProofLoom also achieved the highest mean score in all 16 combinations of task group, evaluation protocol, and model judge.Source: §1 · p. 3
• Across 33 developments, ProofLoom produced 490,693 lines of algorithm-local Lean code with no sorry, and its formalizations exposed 28 discrepancies in published sources across 22 developments.Source: §1 · p. 3
• ProofLoom builds Lean algorithm models and supporting theory from source algorithms, theorems, and proofs, with open proof obligations guiding what to construct next.Signature contracts record revision evidence and derived claims as obligations; Judge rejects unsupported assumptions or weakened theorems, while Planner–Audit checks the proof against the source argument.Source: §1 · pp. 2–3
• SOptLib accumulates verified reusable mathematics and construction records, which later tasks retrieve and extend through a cycle of construction, accumulation, and reuse.Extracted results are generalized and verified; records preserve modeling decisions and failed proof routes.Source: §1 · p. 3

2 Proof-Obligation-Driven Theory Construction

• ProofLoom formalizes the algorithm, target theorem, proof, and required domain infrastructure while recording blockers and reviewing changes to the Lean statement.The resulting objects, assumptions, and conclusion must remain in correspondence with the source.Source: §2 · p. 3

2.1 Constructing Theory from the Target Proof

• Current obligations and proof attempts expose the missing definitions, interfaces, and bridge lemmas; ProofLoom builds and checks this dependency frontier in order.It expands obligations along the source proof and reuses Mathlib and SOptLib where applicable.Source: §2.1 · pp. 3–4, Figure 2 · p. 4
• In stochastic mirror descent, expressing the random-iterate conditional expectation step requires a filtration, adapted iterates, and measurability and sampling relations.The next task is proving the bridge lemma; an oracle interface that cannot express a source dependency supports reconstruction.Source: §2.1 · p. 4

2.2 ProofLoom Pipeline

• The Model stage defines canonical objects, assumptions, updates, stochastic semantics, output rule, and theorem; derived properties remain proof obligations.Construct plans and builds proofs under the protected interface, audits source correspondence, and reviews candidate revisions.Source: §2.2 · pp. 4–5
• After all Lean obligations close, Learn certifies the development and adds reusable mathematics and reviewed construction experience to SOptLib.Retrieved results must be instantiated with their hypotheses proved; missing support can be constructed, generalized, checked, and returned to the library.Source: §2.2 · p. 5

3 Governing Proof--Model Co-evolution

• Signature contracts make model revisions explicit and subject them to review, recording the obligation, source passage, and Lean evidence behind each decision.Derived claims remain obligations, and approved revisions must pass source-correspondence and Lean checks.Source: §3 · p. 5, §3.1 · pp. 5–6

3.1 Signature Contracts for Model Revision

• The Lean model and supporting interfaces may evolve as the proof reveals missing structure, but must preserve the source algorithm, assumptions, and convergence claim.If investigation establishes a source-claim gap, the original statement and evidence are retained and any corrected result is reported separately.Source: §3.1 · pp. 5–6
• Judge checks each added premise against the source, keeps derived facts as proof obligations, and reviews revised objects, bridges, and dependent proofs.For a proximal update, the optimality condition must be derived from the update definition; unfinished proofs remain scheduled obligations.Source: §3.1 · pp. 5–6

3.2 Planner--Audit for Proof Construction

• Planner expands source steps into intermediate claims, while Audit traces Lean dependencies backward to check whether helpers support those steps or add unnecessary branches.Audit can request evidence of failed interfaces, incompatible hypotheses, or missing dependencies before a branch continues.Source: §3.2 · p. 6
• Audit diagnoses the source step and Lean obligation, then Planner revises the blueprint, reuses a result, or reports a blocker for model reconstruction.Recorded failed routes and diagnoses inform later attempts; repairs are tested through Lean proofs or counterexamples.Source: §3.2 · p. 6

3.3 Worked Example: SAM’s Gaussian KL Bridge

• For SAM’s Gaussian KL bridge, the Euclidean-coordinate theorem did not directly fit affine Gaussian representations on a finite-dimensional inner-product space.ProofLoom reconstructed the measurable representation bridge, transported KL divergence, and combined the result with squared-norm preservation to obtain the target identity.Source: §3.3 · p. 7

4 SOptLib: Learning from Algorithm Proofs

• SOptLib combines verified Lean definitions and lemmas with records of modeling decisions, failed routes, revisions, reuse conditions, and supporting evidence.Its completed algorithm developments provide worked examples of the theory.Source: §4 · p. 7
• Extraction generalizes algorithm-specific objects into independent interfaces, proves the results in Lean, and instantiates them in the original development with hypotheses discharged.The original theorem statements and definition types are preserved, and the complete development is rebuilt and independently reviewed before merging.Source: §4 · p. 8
• Later tasks search the library and inspect declarations, hypotheses, dependencies, and construction records before instantiating results.New proof obligations can motivate further library additions through the same process.Source: §4 · p. 8

5.1 Experimental Setup

• The benchmark covers ten FOML algorithms and five research-paper algorithms; each system–task pair receives a cumulative 48-hour generation budget.Source: §5.1 · p. 8

5.2 Main Results

• ProofLoom leads all 16 source-group, protocol, and model-judge combinations, while maintaining high source-faithfulness scores on research papers using SOptLib.Source: §5.2 · pp. 8–9
• 6.3/7 on FOML and 6.4/7 on research-paper tasks, versus Archon’s 4.9/7 and 5.0/7, respectively, in human mean ratings.Source: §5.2 · p. 8, Table 2 · p. 9

5.4 Formalization Products and Source Findings

• The formalization census covers 33 developments: 22 from FOML, eight from research papers, and three from research notes.Source: §5.4 · p. 10

5.3 Mechanism Ablation

• 33 cases are crossed by the full system versus 29 for either ablation; removing Judge raises incorrect repairs from one to six.Source: §5.3 · p. 9, Table 3 · p. 10

• The w/o Planner–Audit row contains 62.1 and 3.4, but this passage does not identify the corresponding measures.Source: A. Model/interface mismatch (n = 29) · p. 10

• 28 independent discrepancies—including incorrect formulas, proof gaps, and algorithm–analysis mismatches—affect 22 developments.Source: B. False/underspecified claims (n = 14) · p. 10
• SAM’s proof invokes a nondecrease premise at a smaller Gaussian scale than the theorem assumes, which need not preserve the inequality.For the supplied smooth bounded loss example, the Gaussian averages are approximately 0.473 at ρ and 0.382 at σ; the corrected formulation requires nondecrease at the selected scale.Source: B. False/underspecified claims (n = 14) · p. 10
• Lan’s proof evaluates a potential outside the feasible set, although smoothness is assumed only on that set.The formalization develops open-domain cocoercivity under an additional convexity assumption on each intrinsic component gradient, then extends the bound to the feasible set.Source: B. False/underspecified claims (n = 14) · p. 10

• Mathlib, Coquelicot, and Isabelle provide analysis and probability foundations, while OptLib formalizes convex analysis and first-order optimization rates.Source: §6 · p. 11
• Prior autoformalization systems address statement and project formalization, retrieval, proof development, and semantic assessment; ProofLoom builds theory from convergence-proof obligations and governs source-facing revisions.The passage contrasts its focus with approaches including Archon, Open Gauss, LeanMarathon, Trellis, and ProofFlow.Source: §6 · p. 11
• Neural theorem proving includes retrieval-augmented proving, learned proof generation and search, benchmark completion, and reusable lemma libraries; SOptLib retains reusable theory and construction records.Source: §6 · p. 11

• Repeated errors in LLM-based semantic review can shift assumptions or conclusions away from the source.Source: §7 · p. 11
• Construction, semantic checks, and audit records require additional model calls and Lean checks, and research-level formalization can take hours.Source: §7 · p. 11
• Evaluation covers textbook and research-paper tasks in stochastic optimization; applicability to more abstract domains and less detailed proofs requires further evaluation.Source: §7 · p. 11

8 Conclusion

• Across textbook and research-paper tasks, ProofLoom earns higher average source-faithfulness scores than evaluated baselines and exposes 28 source errors across 22 developments.Source: §8 · p. 11
• ProofLoom uses Signature contracts and Planner–Audit for source-grounded review, while SOptLib accumulates verified mathematical infrastructure and construction knowledge.Source: §8 · p. 11

A.1 Task Scope and Resources

• The 15 source tasks comprise ten FOML algorithms and five research-paper algorithms, with research tasks sharing fixed FOML-derived support throughout evaluation.Source: §A.1 · p. 15

A.2 Baseline Implementations and Execution Settings

• ProofLoom uses indexed prior SOptLib results for FOML tasks and a fixed FOML-derived SOptLib version for its five research-paper tasks.Source: §A.2 · p. 15
• All systems use GPT-5.5 with high reasoning effort and a 48-hour cumulative generation limit per system–task pair.Source: §A.2 · p. 15
• Raw Codex and Raw Codex (Goals) receive the same task prompt in separate workspaces, using direct Codex execution and the built-in Goals workflow, respectively.Source: §A.2 · pp. 15–16

A.3 Human Evaluation and Adjudication

• Human ratings use a jointly established seven-point rubric: H1 and an independent LLM assess each artifact, with H2 adjudicating disagreements across 105 final ratings.The rubric caps scores for missing source endpoints, incorrect algorithm semantics or conclusions, assumed proof bridges, and incomplete source scope; justified source corrections are assessed under the same rubric.Source: §A.3 · pp. 16–17

A.4 Model-Based Evaluation and Aggregation

• For each 0–100 model-based protocol, four evaluator configurations score anonymized candidates; eligible verified artifacts receive full verification credit, while mathematical and source-alignment scores remain unchanged.G-Eval allocates 25 points each to fidelity, source alignment, theorem derivation, and verification; FidelityEval allocates 40, 40, 15, and 5 points across its four components.Source: §A.4 · pp. 17–18

A.5 Mechanism Ablation Protocol

• Across 43 audited cases, the RAPP example shows the full system repairing an initialization invariant, while removing Judge yields an unsupported restriction and removing Planner–Audit leaves the invariant unfinished.The comparison starts each configuration from the same development state and assesses diagnosis, repair direction, and source alignment rather than removing components from full end-to-end runs.Source: §A.5 · p. 19

A.6 Validation and Reproducibility

• Evaluation outputs are validated for input identity, evidence, candidate coverage, scoring dimensions, and recoverable results, while released data and pinned Lean/Mathlib manifests support reproducing scores and ablation rates.The reproduction package includes an offline command that reconstructs the main scores and mechanism-ablation rates.Source: §A.6 · pp. 19–20

A.7 Corpus Census and Visualization

• The corpus comprises 33 developments and 490,693 physical lines across 60 algorithm Lean files, with no explicit sorry/admit tokens in those files.The census distinguishes physical from code-bearing lines and excludes shared libraries, external theory, caches, and unused copies.Source: §A.7 · p. 20

B.1 Counting, Source Versions, and Evidence

• The audit identifies 28 independent discrepancies across 22 developments, covering incorrect formulas, proof gaps, and algorithm–analysis mismatches, with source versions and repair scope documented.It distinguishes 25 discrepancies in selected source versions from three with later author corrections or published errata.Source: §B.1 · p. 20

A. Discrepancies in the selected sources

• Examples in the selected sources include a predecessor-index error in SNCCG and, in RAPP, a reachable component refresh that can leave the gradient domain.The SNCCG proof uses the current index for a predecessor update; the RAPP case concerns the gradient domain of a refreshed component.Source: A. Discrepancies in the selected sources · p. 21, A03 VRMD / VRAGD / RAPP / RGE · p. 22

A03 VRMD / VRAGD / RAPP / RGE

• The catalogue reports discrepancies involving adaptive conditional centering, fixed-candidate bounds reused after data-dependent selection, output-law transfer, and omitted algorithm clipping across NSAGD, 2-RSGD/2-RSGF, SAMP, SNCGS, and MARS.Source: A03 VRMD / VRAGD / RAPP / RGE · p. 22
• MARS’s simplified variance-reduction parameter loses a momentum factor.Source: A03 VRMD / VRAGD / RAPP / RGE · p. 23

B. Discrepancies with subsequent author revisions

• AMSGrad’s old momentum-weighted telescope is unsupported by the theorem conditions.Source: B. Discrepancies with subsequent… · p. 23
• PULM-DGD’s v1 combined-state update disagrees with the analyzed invariant.Source: B. Discrepancies with subsequent… · p. 23
• PULM-DGD’s v1 Lyapunov combination and absorption change coefficients.Source: B. Discrepancies with subsequent… · p. 23

B.2.1 Textbook Algorithms

• SNCCG’s printed corollary omits a zero-noise initial-gap factor, and its variable-step proof substitutes current for predecessor stepsizes without justification.A concrete instance refutes the universal corollary but not the parent bound; a separate one-step check disproves the printed equality for feasible positive stepsizes.Source: §B.2.1 · p. 23
• The VRMD one-sided Bregman bound needs smoothness beyond the feasible set; its repair adds intrinsic-gradient image convexity, while NSAGD requires conditional oracle guarantees.A published interior-point counterexample violates the inequality. The VRMD repair derives the bound on the relative interior and extends it by continuity; for NSAGD, conditional centering at adaptive queries excludes the constructed marginal-only example.Source: §B.2.1 · pp. 23–24
• NSBMD’s expectation proof loses a factor of two, its literal update assigns a gradient mapping instead of a proximal point, and NVRMD drops a descent term.The corrected NSBMD source-boundary theorem retains (1/2)LHS ≤ RHS; the update check gives a printed bound of 1 ≤ 2/3. NVRMD’s joint bound repairs the proof while preserving its original parameters and b = 17T.Source: §B.2.1 · p. 24
• RAPP can query outside its stated component-function domain, while SAPD’s query and noise center mismatch makes its same-query variance assumption insufficient.The RAPP example reaches 47/36 outside X, so well-definedness requires broader domain assumptions or another invariant. SAPD’s exact-oracle example has zero same-query noise variance but mixed-center squared error one; a corrected expected-gap theorem adds an explicit mismatch budget.Source: §B.2.1 · pp. 24–25

B.2.2 Research-Paper Algorithms

• SAM needs bounded-loss and scale-matched Gaussian premises, PAGE’s printed horizon requires η = ηmax, and Lion’s upper-order schedules do not ensure convergence.The cited SAM example shows the nondecrease premise at ρ need not hold at the selected σ; PAGE’s η = 1/1000 example has expected gradient norm above 0.9 rather than 0.1. Lion’s counterexample satisfies the printed upper-order conditions, while reciprocal-rate conditions repair the endpoint.Source: §B.2.2 · pp. 26–27
• STORM’s final simplification drops parameter dependence, and SPIDER’s theorem names OPTION I while proving OPTION II and separately misstates a finite-sum batch-size substitution.The STORM issue changes explicit parameter dependence, not the displayed powers of T and σ. SPIDER’s output mismatch is distinct from the batch-size formula discrepancy; neither finding establishes that the intended convergence rate is false.Source: §B.2.2 · p. 27
• MARS proofs omit clipping and lose preconditioner and momentum factors in separate recurrence, variance, and parameter-simplification steps.The repairs retain the clipping correction or assume its norm is at most one, preserve ρ² in the variance coefficient, and restore βu in the scalar simplification.Source: §B.2.2 · pp. 27–28

B.3 Category B: Discrepancies with Subsequent Author Revisions

• The selected AMSGrad version has a momentum-weighted telescope gap, and PULM-DGD v1’s update breaks the analyzed invariant; later PULM-DGD v3 corrects the update.The AMSGrad finding is version-specific and does not claim monotonicity is necessary for every analysis. The PULM-DGD v1 counterexample is not attributed to v3, which uses the required +γDg update.Source: §B.3 · pp. 28–29
• The PULM-DGD v1 coefficient combination does not justify its printed absorption constants or admissible stepsize.The proof changes the objective-gap and consensus coefficients, and multiplying Eq. (18) by 24/γ already contributes 192nγLC2 M before descent; author v3 rewrites the stepsize and communication-round conditions, but the v1 defect is retained separately.Source: §B.3 · p. 29

B.4 Repaired Endpoints and Evaluation Scope

• Lean checks cover 17 named A03 declarations, including supporting lemmas and convergence endpoints, with endpoint signatures and dependencies checked.Added domain conditions appear in each algorithm’s setup, while other endpoint premises remain in the statements; Table 8 notes that extension conditions preserve function values and selected gradients on X.Source: §B.4 · p. 29, Table 8 · p. 29

C.1 Formalization Control Loop

• The control loop carries proof states, contracts, Lean outcomes, and reviews between reconstruction and proof construction; certification checks the completed dependency closure.Planner inspects goals and progress, while Audit checks the route against the source proof; remaining obligations accompany handoffs, and certification failures return diagnostics.Source: §C.1 · pp. 30–31

C.2.1 Protected Interfaces and Change Tracking

• Protected signatures and Setup-field types constrain edits, while Audit and endpoint certification check definitions, dependencies, and source correspondence.Hash-based diffs associate changed source-facing heads with blockers and flag undisclosed edits for Judge review.Source: §C.2.1 · p. 31

C.2.2 Revision Contracts and Judge Review

• Revision contracts classify each change as an assumption or derived lemma and provide source citations; Judge rejects unsupported premises and changes to the source claim.A passing review triggers a second independent Judge call; disagreement sends the candidate back for revision.Source: §C.2.2 · pp. 31–32

C.2.3 Endpoint Guarantees and Remaining Obligations

• At the certified endpoint, definitions and proved lemmas preserve source assumptions, but certification still requires completed Lean proofs throughout the target dependency closure.Unresolved lemmas remain visible with supporting evidence for subsequent proof attempts.Source: §C.2.3 · p. 32

C.3 Agent Roles and Prompt Instructions

• The engine separates source packaging, model construction, proof planning, editing, and review; agents use source evidence and live Lean state to direct localized work.Reconstruction prompts require evidence and affected consumers, and distinguish stated assumptions from facts that need proof.Source: §C.3 · pp. 32–33

C.3.1 Operational Judge discipline

• Judge applies a semantic admission policy, while contracts, signature diffs, fresh verification, and endpoint checks provide mechanical containment.The appendix reports the prompt structure and points to the accompanying artifact for its full text and output schema.Source: §C.3.1 · p. 33, Table 9 · p. 33

C.4 Worked Example: SAM’s Gaussian KL Bridge

• The SAM example identifies a mismatch between an arbitrary measurable-space bridge and the Euclidean coordinates required by the available Gaussian KL theorem.The direct transport attempt required extra topological structure; reconstruction makes the source’s Euclidean measurable structure explicit for the bridge and its consumers.Source: §C.4 · p. 33
• The reconstructed measurable equivalence transports the Gaussian KL identity, which Judge accepts and the selected-Gaussian prior-grid proof uses without adding it as a premise.The checked result closes the local calculation for the probability-event construction; the radius bound and remaining event comparisons are separate proof parts.Source: §C.4 · p. 35

D.1 Library Organization and Index

• The SOptLib index links reusable declarations to mathematical concepts, source provenance, applicability, and downstream uses, making results and their conditions discoverable.The module directory describes mathematical scope and dependencies, while the catalog maps declarations to files, layers, and keywords.Source: §D.1 · p. 35

D.2 Retrieval and Use during Formalization

• Agents search from the proof state and target mathematical step, then check candidate signatures and Lean applications; representation differences require a proved bridge.Lexical ranking prioritizes inspection, but signature comparison and Lean checking establish applicability.Source: §D.2 · pp. 35–36

D.3 Extraction, Review, and Integration

• Extraction generalizes reusable objects and arguments from certified developments, proves them in staging, and checks their use in the originating algorithm before integration.Accepted declarations are merged only after review and rebuild checks pass.Source: §D.3 · p. 36

D.4 Evaluation Protocol

• FOML tasks retrieve the library accumulated before they start, while all five research-paper tasks use one fixed version containing only FOML-derived definitions and lemmas.The comparison and ablations assess systems in their specified configurations and examine selected obstructions and final artifact quality.Source: §D.4 · p. 37

D.5 Library Census

• The released SOptLib contains 42 Lean files, 109,634 lines, 2,399 source declaration heads, 1,983 theorems, and 2,294 catalog entries.Separately counted imported local theory and staging support add 6,857 physical lines across 48 distinct file contents.Source: §D.5 · p. 37

D.6 Formalization without SOptLib

• In Table 11, final ratings were similar across configurations, while runs with SOptLib removed used 7.7% more tokens for AMSGrad, 97.5% for SBMD, 51.3% for NSAGD, and 154.0% for NSMD.Each token difference is Removed minus Full; Full retains SOptLib and Removed isolates it after the paired materials are prepared.Source: Table 11 · p. 37, §D.6 · p. 38