arxiv-2510-25427 SRC-0330 · paper

RLMEval: Evaluating Research-Level Neural Theorem Proving

Created: 2025-10-29 · Ingested: 2026-09-19

https://arxiv.org/abs/2510.25427(opens in a new tab)

Despite impressive results on curated benchmarks, the practical impact of large language models (LLMs) on research-level neural theorem proving and proof autoformalization is still limited. We introduce RLMEval, an evaluation suite for these tasks, focusing on research-level mathematics from real-world Lean formalization projects. RLMEval targets the evaluation of neural theorem proving and proof autoformalization on challenging research-level theorems by leveraging real Lean Blueprint formalization projects. Our evaluation of state-of-the-art models on RLMEval, comprising 613 theorems from 6

In brief

Lean provers that clear competition benchmarks largely fail on the main theorems of real research formalization projects. RLMEval collects 613 blueprint theorems (the high-level results linked in a project's informal blueprint, not the auxiliary lemmas that make up 68.3 % of theorems on average) from 6 Lean projects including Carleson, FLT, PFR, PNT, FLT3, and TLB, and evaluates both neural theorem proving and proof autoformalization at pass@128.

DeepSeek-Prover-V2-7B, the best of 5 models tested, reaches 10.3 % on proof autoformalization in normal mode, against its reported 75 %+ on MiniF2F at pass@32. Giving models access to project auxiliary lemmas (easy mode) lifts it to 16.7 %; supplying an informal proof adds only ~1.5 percentage points over bare statement proving (8.8 % to 10.3 %). Success is concentrated on short proofs: winning generations average 2.5–6.0 lines versus 16.6 for humans, and per-project rates run from 32.1 % on FLT3 down to 2.73 % on Carleson, tracking average proof length.

The pass rates are measured, with matched easy/normal and NTP/autoformalization contrasts across all 5 models, plus a sampling sweep from pass@1 to pass@128 showing diminishing gains. Limits acknowledged by the authors: only 7B provers (not DeepSeek-Prover-V2-671B), no pass@8192, in-file context only with no retrieval, and unknown contamination for all models except Llemma-7B.

Treat MiniF2F-style scores as a poor predictor of usefulness in an ongoing formalization project.

Written from the abstract by claude-opus-5 on 2026-10-17, with every figure checked against it. Not a substitute for the paper.

Referenced by

Claims in this catalog that draw on this source, and whether as support or counterpoint.