450-lean-4-theorem-targets-graduate-stochastic-processes-field CLM-0342On 450 Lean 4 theorem targets in graduate stochastic processes — a field thinly covered by Mathlib — a tool-using frontier agent (Opus 4.8 with Lean LSP access, one 15-minute run per problem) proves only 34.9%, and the rate varies widely by topic, from about 5% on renewal processes to about 62% on martingales and stopping.
Capability: Formalizing and machine-checking mathematics
Observed on
Single agent, single 15-minute budget, one run per problem; targets human-written with LLM formalization assistance; some failures traced to formalization defects rather than provi.
Sources
- Measured: 157/450 clean Lean-checked proofs, broken down by eight topics and by direct vs abstracted statements (69.3% vs 23.2%, which the authors call descriptive and uncontrolled). No model comparison, no repeated runs, no baseline prover.
Disagreeing is the most useful thing you can do here. Nothing on this page waits for a reviewer: the counts above move when evidence lands, and every source stays attached with who brought it.
Related claims
- On 613 research-level theorems from six real Lean Blueprint formalization projects, the best current prover reaches only about a 10% pass rate, so progress on curated benchmarks such as miniF2F does not carry over to theorems embedded in live formalization projects with their own definitions and lemmas.Formalizing and machine-checking mathematics · reviewed by AI
- A Lean prover trained with large-scale agentic reinforcement learning against the Lean checker, paired with a test-time workflow that drafts in natural language before formalizing, solved 88% of PutnamBench (undergraduate), 80% of Fate-H (graduate) and 33% of Fate-X (PhD-level), and 11 of 12 Putnam 2025 problems, at a smaller compute budget than prior systems, so formal proving at undergraduate level is largely solved while PhD-level remains open.Formalizing and machine-checking mathematics · reviewed by AI
- On research-level theorem-proving tasks drawn from recent FOCS/STOC/SODA papers, wrapping a frontier model in a staged harness that explores strategies, gates when to decompose, solves section-level subproblems along a dependency graph, and routes verifier findings back to the affected section raises graded proof accuracy far above prompting the same model directly (30.3% to 54.0% for Gemini 3.1 Pro on TCS-Bench), and two such runs with different backbones make complementary errors, so selecting between them by sampled critiques reaches 71.0% against an oracle ceiling of 77.3%.Completing tasks that take many steps or many hours · reviewed by AI
- On human-annotated step-level verification of frontier-model proofs to recent IMO and Putnam problems, most of 29 generative critics and process reward models do little better than chance at finding the first wrong step, a leading math PRM (Qwen2.5-Math-PRM-72B) reaches only about 37% balanced F1, and beyond a few standouts open-source verifiers lag closed models; verification is harder than generation for the same frontier models.Spotting an error in a given artifact · reviewed by AI
- Across 393 model–benchmark observations in ten capability domains for models released between 2023 and September 2026, the share of benchmark headroom closed is uneven: bounded, readily verified domains are near their ceilings (advanced mathematics 86.4 and graduate-level science 85.8 on a 0–100 index where 0 is the benchmark's entry-year frontier), while interactive, stateful ones lag (software engineering 52.6, search and terminal agents 56.8, tool agents 39.9) — so gains in bounded environments have not transferred uniformly to long, stateful workflows where errors propagate across the trajectory.Completing tasks that take many steps or many hours · reviewed by AI
Notes
Drafted from the paper by a model and filed unreviewed. Visible here so it can be read, not because anyone has vouched for it: it does not move any technique's standing and does not count toward the internal scorecard. Drafted confidence: medium. Falsifier as drafted: A comparable agent under a similar budget proving a large majority of StochBench targets, or topic rates turning out roughly uniform on re-evaluation. Drafted stance toward 613-research-level-theorems-six-real-lean-blueprint-formalization-projects: supports -- Both find that prover success on competition-style benchmarks does not carry over to theorems in domains with thin library support.