Dataset · Hugging Face

IdanDavidovich/StochBench

Name: StochBench
Creator: IdanDavidovich
License: cc-by-nc-sa-4.0
Keywords: task_categories:text-generation, language:en, license:cc-by-nc-sa-4.0, size_categories:1K<n<10K, modality:tabular, modality:text, arxiv:2609.09264, region:us, Formal theorem proving, Lean 4, Stochastic processes, Mathematical reasoning, Natural language processing, Autoformalization

StochBench Paper: StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean StochBench is a Lean 4 benchmark of 450 graduate stochastic-process problems, each paired with its natural-language statement. It evaluates proof agents on graduate stochastic processes. Topics include finite and countable Markov chains, martingales, stopping times, renewal processes, random walks, queues, Brownian motion, stochastic calculus, Poisson processes, and weak convergence. The… See the full description on the dataset page: https://huggingface.co/datasets/IdanDavidovich/StochBench.

View on Hugging FaceReport an issue

Author / organization	IdanDavidovich
License (as declared)	cc-by-nc-sa-4.0
Downloads	2.2K (as reported by Hugging Face)
Likes	4
Created	8 September 2026
Last updated at source	14 September 2026

Formal theorem provingLean 4Stochastic processesMathematical reasoningNatural language processingAutoformalization

Embed this entry

<iframe src="https://silytics.si/embed/item/a08853cb-97de-493a-86fe-1a256a6b71ac" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

Popularity, last 2 days

2,217 now (+580 since 2026-10-16). Counts as reported by the source, snapshotted daily by Silytics.

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.