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

arXiv: https://arxiv.org/abs/2609.09264 · HTML: https://mlsanity.com/paper/2609.09264/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 13 of its 43 references that are in the map.
- First posted on arXiv 8 Sep 2026.

## Builds on (most cited first, 13 of 13)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?](https://mlsanity.com/paper/2603.12744/) (2026)
- [FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory](https://mlsanity.com/paper/2510.02335/) (2025)
- [FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?](https://mlsanity.com/paper/2603.26996/) (2026)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [A Formalization of Doob's Martingale Convergence Theorems in mathlib](https://mlsanity.com/paper/2212.05578/) (2022)
- [A Formalization of the Ionescu-Tulcea Theorem in Mathlib](https://mlsanity.com/paper/2506.18616/) (2025)

## Abstract (arXiv)

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.