613-research-level-theorems-six-real-lean-blueprint-formalization-projects CLM-0286observationsingle paperReviewed by AI
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.
Capability: Formalizing and machine-checking mathematics
Observed on
RLMEval, Lean 4, six Blueprint projects, neural theorem proving and proof autoformalization, 2025; state-of-the-art provers of late 2025..
Sources
- Single snapshot; the gap between competition and research-level settings is the durable observation, and Seed-Prover 1.5's later results on Fate-X (33% at PhD level) point the same way.
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 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.Formalizing and machine-checking mathematics · 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
- 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
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 prover exceeding 40% on RLMEval under the same compute budget, or evidence the projects' contexts were not provided fairly.