Primary evidence
- StochBench: A Domain-Specific Benchmark for Stochastic Processes in LeanS1 · Primary research · Paper · 2026-09-08
- StochBench datasetS1 · Primary research · Dataset
StochBench brings graduate stochastic processes into Lean theorem-proving evaluation
The benchmark covers Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, Poisson processes and continuous-time Markov processes.
What happened?
The StochBench paper introduced 450 Lean 4 problems in graduate stochastic processes paired with natural-language sources; the authors report that an Opus 4.8-based proof agent solved 157 of 450 targets within a 15-minute per-problem budget, a 34.9% proof rate.
The benchmark covers Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, Poisson processes and continuous-time Markov processes. Its released dataset distinguishes 114 direct formalizations from 336 abstracted targets that expose assumptions explicitly when the required stochastic-process infrastructure is not available in the fixed Lean/Mathlib environment.
Why it matters
Formal theorem-proving benchmarks can overstate general mathematical coverage when they concentrate on domains already well represented in proof libraries. StochBench makes domain breadth and library-support limitations part of the evaluation surface, providing a harder test of whether proof agents can operate in applied mathematics with substantial formalization gaps.
Significance rationale: StochBench is a field-level benchmark milestone because it moves Lean theorem-proving evaluation beyond predominantly competition and textbook-style mathematics into a broad graduate applied-mathematics domain, while explicitly representing the gap between direct formalization and abstraction needed when library support is incomplete.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Substantive AI support
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Informal, Formal, Hybrid
- AI contribution
- An Opus 4.8-based formalizer assisted in expressing human-written benchmark problems as Lean statements, with Lean feedback and human revision, and an Opus 4.8-based proof agent supplied the reported baseline proofs.
- Human contribution
- Researchers selected and wrote the benchmark-specific problems, definitions, hypotheses and evaluation protocol, reviewed the formal statements against their source problems, fixed the Lean/Mathlib environment and analyzed the baseline results by topic and representation.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-14
Technical details
- Systems
- stochbench, lean
- Organizations
- case-western-reserve-university
- Problems
- stochastic-processes, graduate-applied-mathematics
- Methods
- benchmarking, lean-formalization, proof-agents, autoformalization
Sources & artifacts
- StochBench: A Domain-Specific Benchmark for Stochastic Processes in LeanS1 · Primary research · Paper · accessed 2026-09-14
- StochBench datasetS1 · Primary research · Dataset · accessed 2026-09-14
- StochBench Lean 4 benchmark datasetArtifact · Benchmark
Verification history
- 2026-09-08 · Paper released · E2 · Research record
The arXiv research record defines the 450-problem benchmark, its stochastic-process scope and the reported 157/450 baseline under a 15-minute per-problem budget.
- 2026-09-14 · Paper released · E3 · Inspectable artifact
The public StochBench dataset exposes the informal statements, Lean statements, representation labels and stored proof records. E3 records artifact-level inspectability and does not imply an independent replay of the full baseline evaluation.
Corrections
No corrections recorded.