Summary

• STOCHBENCH is a new Lean 4 benchmark containing 450 graduate-level stochastic processes problems, each paired with its natural-language source, spanning eight topics from Markov chains to stochastic calculus.
• The benchmark comprises 114 direct (using Mathlib/shared definitions) and 336 abstracted (properties taken as hypotheses) targets, addressing a field underrepresented in Mathlib.
• An Opus 4.8-based proof agent achieves a 34.9% clean proof rate (157/450) under a 15-minute per-problem limit, with rates varying dramatically by topic (4.9% for renewal processes to 61.7% for martingales & stopping).
• The benchmark includes shared mathematical definitions for recurring concepts (matrix representations, hitting solutions, return times, etc.) and distinguishes between marginal distributions and joint process laws in problem representation.
• STOCHBENCH is released publicly with JSON records containing identifiers, informal statements, Lean targets, and representation labels, along with shared definitions and baseline proof attempts.

Introduction and Theoretical Foundation

The paper addresses a gap in formal theorem proving benchmarks: existing benchmarks (MINIF2F, PROOFNET, PUTNAMBENCH, FORMALMATH) are dominated by competition math (IMO, Putnam) or broad textbook collections that poorly represent field-specific applications. The authors argue that aggregate scores across diverse problems can obscure domain-specific strengths and failures of automated provers.

The theoretical foundation rests on Lean 4 and Mathlib, which provide an extensible proof environment with reusable mathematical abstractions. The field of stochastic processes was chosen because:

• It is central to statistics and machine learning
• It has substantial but incomplete formalization in Mathlib (e.g., Brownian motion, martingale convergence theorems, Itô integrals are formalized, but many graduate-level results are missing)
• It requires recurring argument patterns (first-step analysis, martingale arguments, coupling, etc.) that provide a meaningful test of proof automation

The benchmark design distinguishes between:

• Direct targets: use Mathlib objects or shared definitions directly
• Abstracted targets: take required properties as hypotheses when infrastructure is unavailable

This distinction addresses the reality that some problems require infrastructure not yet in Mathlib, while still allowing Lean to verify that conclusions follow from stated hypotheses.

Methodology

Problem Selection and Curation

The authors combined problems written specifically for the benchmark with exercises selected from:

• Probability, Mathematical Statistics, and Stochastic Processes (Siegrist, 2022)
• MIT course notes: Introduction to Stochastic Processes (Wu, 2015), Advanced Stochastic Processes (Gamarnik, 2013), Discrete Stochastic Processes (Gallager, 2011)

Problems were selected for relevance to stochastic processes; statements closer to general probability theory were excluded. All definitions, hypotheses, and questions are human-written, with an Opus 4.8-based formalizer assisting in expressing problems as Lean theorem statements.

Shared Mathematical Definitions

Recurring concepts were formalized as shared abstractions:

• Finite-state chains: matrix representations for stochasticity, stationarity, irreducibility, aperiodicity, detailed balance, time reversal, total-variation distance
• Hitting times: IsHittingSolution and returnTime express first-step equations
• Transition powers: nstep defines powers through infinite sums for countable-state formulations
• Stopping times: natStop converts natural-valued stopping times to WithTop
• Running maxima: runningMax expresses finite running maxima
• Conditional increments: IsConstDrift states conditional increment identities

Process Law Representations

The benchmark distinguishes two key representations:

HasMatrixMarginals: relates the distribution of $X_n$ to the corresponding row of $P^n$.

HasChainLaw: specifies finite-dimensional probabilities through:

$$\mathbb{P}_\mu(X_0 = x_0, \ldots, X_n = x_n) = \nu(x_0) \prod_{i=0}^{n-1} P(x_i, x_{i+1})$$

Formalization Scope

• Direct targets use Mathlib objects or shared definitions
• Abstracted targets take required properties as hypotheses (e.g., memorylessness assumed rather than derived from continuous-time chain dynamics)

Evaluation Setup

A multi-turn tool-using Opus 4.8-based agent using lean4skills and the Lean LSP MCP server was evaluated with:

• One run per target, capped at 15 minutes
• Allowed: Lean-error inspection, library/shared-definition search, loogle and leansearch queries, proof revisions
• A proof is clean if Lean accepts it without sorry, sorryAx, or additional admitted facts

Empirical Validation / Results

Overall Performance

Clean-proof rates by target class: Direct targets: 69.3%, Abstracted targets: 23.2%.

Key Findings

1. Direct targets are dramatically easier (69.3% vs. 23.2% clean proof rate), though the authors note this comparison is descriptive, not a controlled causal effect—abstraction effects are confounded with problem difficulty and library support.
2. Martingales & stopping achieved the highest rate (61.7%), likely due to strong Mathlib support for martingale theory.
3. Renewal processes were the hardest (4.9%), reflecting poor library infrastructure.
4. Brownian motion & stochastic calculus also proved difficult (17.8%), despite existing formalizations, suggesting interface complexity.

Qualitative Failure Analysis

The authors identified three categories of proof-search failures:

• Plausible targets where the agent failed to find proofs
• Missing lemmas or difficult library interfaces
• Formalization defects: missing measurability, integrability, or non-emptiness assumptions

Theoretical and Practical Implications

For Formal Proof Automation

• STOCHBENCH reveals that domain-specific evaluation uncovers performance patterns invisible in aggregate benchmarks—the 14× spread in proof rates across topics (4.9% to 61.7%) demonstrates this clearly.
• The large gap between direct and abstracted targets suggests that library infrastructure quality is a primary bottleneck for automated proving, not just reasoning ability.
• The benchmark provides supervision data (successfully checked baseline proofs) for training proof-generation models and autoformalization systems.

For Mathlib Development

• The benchmark identifies specific infrastructure gaps in Mathlib for stochastic processes: renewal theory, continuous-time Markov chains, queueing theory, and stochastic calculus interfaces are underrepresented.
• The shared definitions (e.g., IsHittingSolution, HasChainLaw) represent reusable abstractions that could be integrated into Mathlib.

For Benchmark Design

• The direct/abstracted distinction offers a principled way to benchmark problems whose infrastructure is incomplete, without excluding them entirely.
• The informal–formal pairing supports autoformalization research, addressing the semantic alignment problem highlighted by prior work (FORMALALIGN, MATHATLAS).

Conclusion

STOCHBENCH provides a focused testbed for evaluating proof agents on graduate stochastic processes, a mathematically rich and practically important domain previously underrepresented in formal theorem-proving benchmarks. With 450 Lean 4 targets across eight topics at varying abstraction levels, it better represents domain-specific applied mathematics while remaining challenging: the best baseline achieves only 34.9% overall proof rate.

The authors acknowledge limitations: human curation introduces bias, faithfulness review could benefit from peer scrutiny, and the topic/abstraction classifications lack rigorous formal definitions. The direct/abstracted performance comparison is descriptive rather than causal.

Future directions implied by this work include:

• Developing stronger domain-specific provers trained on the released supervision data
• Using the informal–formal pairs for autoformalization training
• Continuing the formalization of stochastic processes in Lean, guided by the identified infrastructure gaps
• Expanding peer review of the benchmark's faithfulness to source problems

The benchmark is publicly available at https://huggingface.co/datasets/IdanDavidovich/StochBench.