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

Feiming Wang; Daibo Li; Kun Yuan

cs.AISep 28, 2026

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

Authors: Feiming Wang, Daibo Li, Kun Yuan

Organizations: Nankai University · Peking University

Abstract

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.

Figures & tables

Figure 1 : Two construction orders. Bottom-up methods build theory first; ProofLoom constructs definitions, interfaces, and lemmas as required by the target proof.

Figure 2 : ProofLoom system overview. Model defines the algorithm and theorem; Construct builds proofs and reviews revisions; Learn certifies developments and updates SOptLib.

Layer	Role	Representative example
Glue	Mathlib bridges	$\mathbb{E}[X\mid\mathcal{F}]=Y\ \text{a.s.}\ \Rightarrow\ \mathbb{E}[X]=\mathbb{E}[Y]$ Integrating a conditional identity
Model	Shared objects	$V_{h}(x,y)=h(y)-h(x)-\langle\nabla h(x),y-x\rangle$ Bregman divergence
Layer 0	Problem properties	$\mathbb{E}\lVert\bar{\delta}_{m}\rVert^{2}\leq\sigma^{2}/m$ Second-moment bound for averaged oracle noise
Layer 1	Convergence lemmas	$\gamma\langle g,x^{+}-u\rangle\leq V_{h}(x,u)-V_{h}(x,x^{+})-V_{h}(x^{+},u)$ Proximal three-point inequality

Table 1 : Mathematical organization of SOptLib with representative examples.

	Human	G-Eval				FidelityEval
System	(1–7) $\uparrow$	GPT 5.6- sol	Gemini 3.8 Flash	DeepSeek V4 Pro	Claude Opus 5	GPT 5.6- sol	Gemini 3.8 Flash	DeepSeek V4 Pro	Claude Opus 5
Raw Codex	2.8	36.5	36.7	37.6	39.9	31.4	28.4	34.3	29.5
Raw Codex (Goals)	3.0	35.3	36.2	36.2	41.3	30.9	29.4	35.7	29.0
OpenGauss	3.5	43.8	48.1	47.6	48.1	43.1	35.9	44.9	36.7
LeanMarathon	4.4	72.9	74.3	75.9	72.4	72.1	64.6	77.0	69.3
Trellis	4.5	63.1	67.2	66.5	65.6	67.0	64.9	64.8	60.9

Table 2 : Seven-system comparison across human and model-based evaluation. Human ratings use a 1–7 scale; G-Eval and FidelityEval scores use a 0–100 scale (higher is better).

Figure 5

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

System	Revision	Workflow and runtime adaptation
Trellis	723bf99d0834	Native setup and proof workflow; source TeX and target labels are prepared as reference inputs.
LeanMarathon	9ace81e67b55	Blueprinter, Target-Reviewer/Refiner, and Worker/Refiner stages; local Git and issue tracking support execution.
Archon	5e9ae7615efa	Initialization, dependency graph construction, and the plan–prove–review loop, starting from a blueprint scaffold.
OpenGauss	f87633900ae1	/autoformalize with source-coverage and verification instructions; noninteractive Codex execution replaces the terminal interface.

Appendix

Table 4 : Baseline repository revisions and benchmark adaptations. OpenGauss uses lean4-skills revision e63d0723bbc9 .

Score	Criteria
1	Missing, unrelated, or plainly wrong formalization of the target algorithm or source result.
2	Names, definitions, comments, or a theorem shell are present; the algorithm update or target conclusion is absent, or the endpoint relies on an unverified placeholder.
3	Some algorithm objects and algebra are present, while a core semantic component is missing and the central derivation remains incomplete.
4	The algorithm and endpoint follow the source structure and compile, while a central bridge is assumed or opaque, or the update, randomness, quantifiers, or conclusion is materially simplified or changed.
5	The algorithm, source assumptions, and endpoint are substantially recognizable, and most of the proof chain is checked; a central closure or alignment condition remains unresolved or explicitly retained as a proof boundary.
6	The algorithm and endpoint are faithful, and the core chain is checked: update, one-step inequality, telescoping/output, stochastic cancellation or variance, and final bound. The endpoint uses accepted standard foundations. Remaining issues are local scope restrictions, visible specializations, domain regularity caveats, or a small number of noncentral hidden source assumptions.

Appendix

Table 5 : Shared rubric for the independent human and LLM ratings and expert adjudication. Reviewers assign the highest level whose conditions are satisfied, then apply the score caps described below.

Protocol	Input	Primary endpoint	Role
Human review	Artifact + source	1–7 adjudicated rating	Artifact quality
G-Eval	Seven candidates + source	0–100 joint score	Artifact quality
FidelityEval	Seven candidates + source	0–100 joint score	Artifact quality

Appendix

Table 6 : Evaluation protocols. Human ratings and the two model-based protocols retain separate scales and aggregates.

ID	Development	Discrepancy	Evidence scope
A. Discrepancies in the selected sources
A01	SNCCG	Corollary 7.12 drops a factor when specializing the stepsize.	Run counterexample
A02	SNCCG	The variable-step proof uses the current index for a predecessor update.	Proof step
A03	VRMD / VRAGD / RAPP / RGE	A one-sided Bregman bound exceeds the constrained-domain hypotheses.	Lemma counterexample
A04	NSAGD	Marginal oracle moments do not justify adaptive conditional centering.	Assumption gap
A05	NSBMD	Taking expectation removes a factor $1/2$ from the descent term.	Proof step

Appendix

Table 7 : Complete catalogue of counted source discrepancies. IDs identify independent issues; multiple algorithms sharing one issue appear in the same row. Evidence types describe the scope of the finding, not a uniform claim that final convergence theorems are false.

Development	Endpoint scope	Repair condition and proof status
VRMD	Theorem 5.6; Corollary 5.8 and its complexity bound	Each $g_{i}(\operatorname{ri}(X))$ is convex. The repaired bounds are proved.
VRAGD	Theorem 5.9; corrected-core Corollary 5.10; scalar-handoff Corollary 5.11	Each component admits a convex smooth extension preserving $L_{i}$ . These endpoint variants are proved under their stated premises.
RAPP	Source-domain-corrected Theorem 6.17; outer-prefix variant of Theorem 6.16	Each regularized subproblem admits a convex smooth extension preserving $L_{i}+2\mu$ . The variants retain their source-domain and initialization premises.
RGE	Canonical-policy Theorem 5.4	Components with $L_{i}>0$ admit convex smooth extensions preserving the original norm and $L_{i}$ . The endpoint is proved.
SAPD (evaluated)	Theorem 4.8(a,b), source-level claims	The artifact identifies the oracle-query mismatch and proves bounds under explicit premises. The full expected-gap and tail claims remain proof targets; the light-tail condition is represented by an opaque predicate.

Appendix

Table 8 : Endpoint status for A03 and SAPD. Extension conditions preserve function values and selected gradients on

X

. A03 repairs add explicit mathematical premises to the selected endpoint statements.

Figure 4 : Signature contracts for model revision. A blocker focuses reconstruction on specific declarations and source evidence. Judge checks the candidate and directs further revisions; the review state retains changes, affected dependencies, and remaining proof obligations.

Panel of Figure 5 — Figure 5 : Agent roles and review loops. Roles are grouped by pipeline stage. Model combines object-model refactoring with a modeling audit and an alignment judge. The Reconstruct / Refactor panel contains the Planner–Prover–Audit proof loop and the blocker-triggered Refactor–Judge contract loop. Certify combines independent semantic audits with adjudication and a localized revision loop; Learn reviews reusable declarations before integration. The upstream Source producer supplies the source package to Model. Arrows summarize handoffs; execution follows the applicable review verdicts and build checks.

Input	Source text, current Lean state, blocker, prior reviews, and compilation status.
Decision	Return either matches_paper or needs_more_refactor .
Faithfulness	Preserve the source-facing theorem head; classify every new premise and record affected downstream consumers.
Proof handoff	Require a proved surrogate, a compiler-grounded voucher, or a source-grounded literature debt for each remaining root cause.
Failure rule	Fail closed when the structural cause, source evidence, or next proof route is unresolved.

Appendix

Table 9 : Structure of the Phase 2b Judge prompt.

Concept	Mathematical statement and informal meaning.
Layer / gap	Library layer and the proof obligation addressed.
Proof idea	Short route description and decisive APIs.
Source	Mathlib, SOptLib, or source-theorem provenance.
Used in	Downstream proof steps and algorithm families.
Origin	Algorithm that motivated the reusable entry and, when available, its search note.

Appendix

Table 10 : Fields in the natural-language index attached to an SOptLib declaration.

Explore similar work

Jun 2, 2026cs.AI

Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries. We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines, which encourages monolithic or ad hoc proof scripts rather than library-quality artifacts. Existing approaches to proof-quality improvement often rely on explicit, computable optimization objectives. In practice, however, the most tractable and experimentally validated objectives are largely length-based, while higher-level qualities such as readability, modularity, maintainability, and reusability are difficult to reduce to reliable automatic metrics. Instead of optimizing proof improvement against a single proxy metric, we take a process-guided approach inspired by human proof-refactoring workflows. We propose an agentic framework

\textbf{Proof-Refactor}

that decomposes proof refactoring into four phases: extracting candidate proof fragments, designing helper declarations, formally proving the extracted and designed components, and repairing the original proof using the verified components. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves rubric-based refactoring scores over a strong Claude Code refactoring baseline, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve proof structure without treating proof length as the primary objective.

Yiming Fu, Peixuan Liu, Zichen Wang +1

Department of Mathematics Southern University of Science and Technology · School of Mathematical Sciences Peking University · Center for Machine Learning Research Peking University

Theorem Proving Proof Code Refactoring LLM Reasoning Strategies Data Generation Pipelines Rubric-Based Scoring+2

Ask PDF

Jun 12, 2026cs.CL

Evaluating the Robustness of Proof Autoformalization in Lean 4

Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have developed LLM-based models for proof autoformalization. However, existing evaluations have typically focused on translating well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations and evaluate robustness under each: a global perturbation paraphrases the informal proof in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original one or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations. Code and data are available via https://github.com/ucr-rai/robust-proof-autoformalization.

Zhengtao Gui, Sheng Yang, Zhouxing Shi

University of California, Irvine · University of California, Riverside

Autoformalization Theorem Proving Proof

Ask PDF

Sep 8, 2026cs.CL

StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean

Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field-specific applications. We introduce StochBench, a Lean 4 benchmark of 450 graduate stochastic-processes problems at varying abstraction levels, each paired with its natural-language source. Addressing a field underrepresented in Mathlib, it covers finite and countable Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous-time Markov processes. Our Opus 4.8-based agent achieves a 34.9% proof rate (157/450) under a 15-minute per-problem limit. StochBench better represents domain-specific applied mathematics while remaining challenging for advanced provers.

Idan Davidovich, Debargha Ganguly, Vikash Singh +1

Case Western Reserve University

Theorem Proving Stochastic Processes Stochastic Differential Equations

Ask PDF