1-000-lean-4-targets-computational-applied-mathematics-textbooks CLM-0281observationsingle paperReviewed by AI
On 1,000 Lean 4 targets from computational and applied mathematics textbooks (optimization, numerical linear algebra, numerical analysis), whose statements depend on locally introduced definitions, current provers solve about 62-72% of a 200-problem sample, so applied-math formalization is tractable but not saturated and requires recovering textbook context to state problems faithfully.
Capability: Formalizing and machine-checking mathematics
Observed on
CAM-Bench, Lean 4, 2026; sample of 200 instances; provers M2F (71.5%) and Aristotle (62.5%); statements validated by compilation and semantic review..
Sources
- New benchmark, partial evaluation (200 of 1,000); the context-dependence of applied problems is the design point, not a measured effect.
Either way, bring evidence: a link, or what you saw.
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 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
- On 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.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
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: Provers near 95% on the full set, or semantic review showing many targets diverge from the textbook exercises.