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

• Competition and broad textbook benchmarks can obscure domain-specific strengths and failures through aggregate scores.Source: §1 · p. 1
• STOCHBENCH provides a Lean 4 benchmark focused on graduate stochastic processes, a field central to statistics and machine learning.Source: §1 · p. 1
• The benchmark releases 450 theorem targets paired with informal statements, shared definitions, and baseline proof attempts.Source: §1 · p. 1
• Its construction combines mathematician-led curation, LLM-assisted formalization, and shared definitions across eight topics.Source: Figure 1 · p. 2

• MINIF2F, PROOFNET, PUTNAMBENCH, and FORMALMATH broaden Lean evaluation across competition difficulty, curricular coverage, scale, and disciplinary coverage.Source: §2 · p. 2
• Lean 4 and Mathlib provide extensible proof environments and reusable abstractions for automated mathematical reasoning.Source: §2 · p. 2
• Proof systems such as LeanDojo, Lean Copilot, Lean-Star, and DeepSeek-Prover combine interaction, retrieval, tactic suggestion, or proof search.Source: §2 · pp. 2–3
• Existing formalizations cover martingale convergence, trajectory-space probability measures, Markov kernels, Brownian motion, and stochastic integration.Source: §2 · p. 2

Sources and selection

• The corpus contains 450 stochastic-process targets selected from benchmark problems, textbooks, exercises, lemmas, theorems, and course materials.Source: §3 · p. 3
• The corpus covers eight topics and excludes claims closer to general probability theory, such as the triangle inequality for total variation distance.Source: §3 · p. 3

Statement construction

• All benchmark-specific definitions, hypotheses, and questions are human-written, while an Opus 4.8-based formalizer assisted with Lean theorem statements.Source: §3 · p. 3

Shared mathematical definitions

• Shared definitions encode recurring concepts including finite-state chain properties, first-step equations, stopping-time conversion, running maxima, and conditional drift.Source: §3 · p. 3

Marginals and joint process laws

• The benchmark distinguishes one-time marginals from joint process laws to specify which process information is available to the prover.Source: §3 · p. 3

Formalization scope

• Direct targets use Mathlib objects or shared definitions, whereas abstracted targets take required properties as hypotheses.Source: §3 · p. 3

Path properties and convergence

• Path and convergence targets state requirements explicitly, including Gaussian increments, independence, path continuity, mean-square convergence, and convergence of bounded continuous expectations.Source: §3 · p. 3

Human review and release

• The release includes theorem records, shared definitions, and baseline proof attempts, but not complete proofs for all targets.Source: §3 · p. 4

• The Opus 4.8-based agent received one tool-using run per target capped at 15 minutes.Source: §4 · p. 4
• The baseline is a single-agent, single-budget evaluation rather than a model comparison or repeated-run study.Source: §4 · p. 4
• 157 clean proofs were produced out of 450 targets.Clean proofs were accepted by Lean without sorry, sorryAx, or additional admitted facts.Source: §4 · p. 4
• Observed failures involved proof search, missing lemmas or difficult library interfaces, and formalization defects such as missing measurability or integrability assumptions.Source: §4 · p. 4

• Human curators decide question curation, faithfulness review, and topic and direct/abstracted classifications, introducing some bias.Source: §5 · p. 4
• The corresponding terminologies were not rigorously defined within the scope of this work.Source: §5 · p. 4
• The benchmark’s informal–formal pairs can support autoformalization training, while checked baseline proofs can supervise proof generation.Source: §5 · p. 4
• Shared definitions and benchmark resources support developing domain-specific provers and continuing stochastic-process formalization in Lean.Source: §5 · p. 4

• The agent-generated proof was obtained in a separate run lasting more than 30 minutes, outside the 15-minute baseline protocol.Source: §A.1 · p. 7
• The target supplies first-step equations through IsHittingSolution rather than constructing hitting-time random variables.Source: §A.1 · p. 7
• The generated Q361 proof develops nine auxiliary theorems across multiple abstraction levels for a single inequality.Source: §A.1 · p. 7
• The proof establishes nonnegativity, positive-reachability closure, and a maximum-principle propagation lemma for finite-state transition matrices.Source: §A.1 · pp. 7–8
• A return-time identity yields harmonicity of Kemeny’s function, whose constancy follows from irreducibility and the maximum principle.Source: §A.1 · pp. 7, 9
• The same propagation lemmas establish a hitting-time triangle inequality, and stationary averaging combines these results into a pointwise bound.Source: §A.1 · p. 7
• The example tests hierarchical proof search by requiring reusable intermediate statements and coordinated auxiliary-theorem dependencies beyond local tactic selection.Source: §A.1 · p. 7

• The direct proof was obtained in a separate run lasting less than 15 minutes.Source: §A.2 · p. 12
• The Q222 target asks for a stationary probability measure π with strictly positive mass on every state of an irreducible finite chain.Source: §A.2 · p. 12
• The proof represents the chain with a real transition matrix whose stochasticity and irreducibility encode nonnegative entries, unit row sums, and positive-power reachability.Source: §A.2 · p. 12
• Transition iterates and their Cesàro averages remain in the standard simplex.Source: §A.2 · pp. 13–14
• A telescoping identity shows that applying the transition map to a Cesàro average differs from it by a term tending to zero.Source: §A.2 · pp. 14–15
• Compactness supplies a convergent subsequence of the averages, and the vanishing difference identifies its limit as stationary.Source: §A.2 · p. 15
• Irreducibility and stationarity under matrix powers then show that every coordinate of the stationary distribution is strictly positive.Source: §A.2 · pp. 15–16

• The example’s agent-generated proof was obtained in a separate run lasting less than 15 minutes.Source: §A.3 · p. 16
• Q128 asks to show that removing drift from Brownian motion yields a martingale and that its variance-corrected square is also a martingale.Source: §A.3 · p. 16
• The Lean statement models a real-valued process on a probability space with filtration, adaptedness, and first- and second-moment integrability assumptions.Source: §A.3 · pp. 16–17
• For 0 ≤ s ≤ t, the abstraction supplies Gaussian increments with law N(0,t−s) and independence from the earlier filtration.Source: §A.3 · pp. 16–17
• The proof derives the conditional-expectation identity for the drift-removed process from the zero conditional increment mean.Source: §A.3 · p. 17
• The squared-process identity additionally uses the conditional second moment and integrability of the cross term before deterministic scaling and subtraction.Source: §A.3 · pp. 17–18, Figure 4 · p. 19