StochBench 发布：450 道研究生级随机过程 Lean 题，把 theorem-proving benchmark 推向应用数学领域

StochBench 提出 450 道 graduate-level stochastic-processes Lean 4 problems，每题与自然语言原题配对，覆盖有限与可数 Markov chains、renewal processes、random walks、martingales、stopping times、queues、Brownian motion、stochastic calculus、weak convergence、Poisson 与 continuous-time Markov processes。论文报告 Opus 4.8-based proof agent 在每题 15 分钟预算下解决 157/450（34.9%），并公开 benchmark dataset 供 proof generation 与 autoformalization 研究使用。