RLMEval: Evaluating Research-Level Neural Theorem Proving

AI summary

Overview

Research area: Automated reasoning and formal mathematics — specifically neural theorem proving (NTP) and proof autoformalization with large language models in the Lean 4 proof assistant.

Technical level: Advanced. The paper assumes familiarity with proof assistants, Lean blueprints, pass@k evaluation, and LLM-based code/proof generation. The conceptual points are accessible, but the experimental setup and results require background knowledge.

Scope: The paper introduces RLMEval, a 613-theorem benchmark drawn from six real-world Lean formalization projects, and shows through evaluation of five state-of-the-art provers that current models perform far worse on research-level mathematics than on established benchmarks like MiniF2F.

What This Paper Is About

Existing benchmarks for LLM-based theorem proving — MiniF2F, ProofNet, PutnamBench — are built mostly from competition-style or textbook problems, and many are now saturated or contain formalization errors. As a result, high scores on these benchmarks do not reliably indicate whether a model can help a mathematician working on an actual formalization project. The paper builds a new evaluation suite from theorems that appear in real Lean Blueprints (the informal-to-formal dependency graph a project author writes), and uses it to measure how far current provers really are from being useful on live research mathematics.

Key Contributions

1. RLMEval benchmark. A suite of 613 theorems from six Lean Blueprint projects spanning analysis, number theory, combinatorics, analytic number theory, and probability/information theory. It targets blueprint theorems — the high-level results that correspond to theorems in a research paper — rather than the auxiliary lemmas that make up roughly 68–86% of the theorems in these projects.

2. Two tasks under one benchmark. RLMEval evaluates both neural theorem proving (given a formal statement, produce a Lean proof) and proof autoformalization (given an informal proof plus the formal statement, produce a Lean proof), whereas most prior benchmarks emphasize only one.

3. Two difficulty modes. Easy mode gives the model access to all definitions and auxiliary lemmas in the source project; normal mode restricts access to blueprint theorems only, forcing the model to rediscover intermediate results. This separates raw proving ability from the ability to reuse project-specific machinery.

4. LeanInteract and multi-version support. A Python interface to Lean's REPL, backported to 41 Lean versions between v4.7.0-rc1 and v4.19.0. This lets RLMEval run against ongoing projects pinned to different Lean releases, unlike tools such as LeanDojo or Pantograph that are tied to specific versions.

5. Systematic model evaluation. A pass@128 evaluation of Llemma-7B, DeepSeek-Prover-V1.5-RL, DeepSeek-Prover-V2-7B, Goedel-Prover-SFT, and KiminaProver-7B, with per-project and per-mode breakdowns.

Main Findings

• Large gap versus curated benchmarks. DeepSeek-Prover-V2-7B, the strongest model tested, reaches only 10.3% pass@128 on proof autoformalization in normal mode, compared with 75%+ reported on MiniF2F under a smaller sampling budget.

• Access to auxiliary lemmas matters a lot. Every model improves in easy mode. DeepSeek-Prover-V2-7B goes from 8.8% to 14.7% on NTP and from 10.3% to 16.7% on autoformalization — a swing of up to roughly 6 percentage points.

• Informal proofs help, but only slightly. Supplying the human-written informal proof alongside the formal statement gives DeepSeek-Prover-V2-7B about a 1.5 percentage-point gain (8.8% to 10.3% in normal mode), suggesting models cannot yet extract much signal from terse, project-dependent mathematical prose.

• Difficulty varies sharply by project. FLT3 (Fermat's Last Theorem for n=3) is the most tractable, topping out at 32.1% for DeepSeek-Prover-V2-7B, while Carleson — a hard harmonic-analysis project — caps out at 2.73%. Proof length in the project correlates well with this ordering: FLT3 < TLB < FLT < PNT < PFR < Carleson.

• Successful machine proofs are short. Successful model-generated proofs average 2.5–6.0 lines against a 16.6-line human average. Models largely succeed on the theorems that admit concise strategies. DeepSeek-Prover-V2-7B is an outlier, producing verbose proofs averaging 6.0 lines with a maximum of 111.

• Sampling gains diminish. Pass rate rises with more samples, but the curve flattens noticeably, unlike on MiniF2F where aggressive sampling (pass@8192) yields large jumps. Brute-force sampling alone will not close the gap.

• Baseline model behavior. Llemma-7B, a general math-pretrained model, is competitive at low sampling budgets but falls behind Lean-specialized models at pass@128, confirming that proof-search fine-tuning matters.

Methodology in Plain English

The authors did not write new theorems. Instead, they harvested existing Lean Blueprint projects — repositories where mathematicians have already formalized research-level results and linked each formal theorem to its informal counterpart. From these, they kept only the "blueprint" theorems: the ones the project author flagged as significant steps. This selection filters out the thousands of small helper lemmas that normally inflate benchmark scores.

Each theorem becomes an evaluation item in two forms. For the theorem-proving task, the model sees the formal statement and the file context preceding it, and must emit a Lean proof. For the autoformalization task, the model also sees the human-written informal proof. The generated proof is checked by Lean itself — there is no partial credit, and no LLM judge.

To make the benchmark comparable across projects that use different Lean releases, the authors built LeanInteract, a Python wrapper over Lean's REPL, and backported its features to every Lean version from v4.7.0-rc1 through v4.19.0. This avoids the heavy project-tracing step that tools like LeanDojo require.

Generation uses sampling with each model's officially recommended temperature and top-p settings, 128 samples per theorem, served through vLLM on H100 GPUs. Results are reported as pass@1, pass@32, and pass@128, broken down by project and by mode. The authors also measured proof length distributions for successful generations as a proxy for problem difficulty.

Why This Matters

Impact on research. The paper argues that benchmark progress in neural theorem proving has decoupled from practical usefulness. By shifting evaluation from competition problems to theorems that appear in active formalization projects, it gives the field a target that is harder to game, harder to memorize, and closer to what a working mathematician actually needs. The clear separation between easy and normal modes also isolates a specific research problem — automated lemma discovery and premise selection — as a lever for improvement.

Real-world applications:

• Assisting formalization projects. Mathematicians working on Lean Blueprints (e.g., ongoing efforts around the sphere packing problem, the Prime Number Theorem, or Fermat's Last Theorem) could use provers to discharge intermediate steps, but only if the models are reliable on exactly the kind of theorem RLMEval measures.

• Verification of machine-generated mathematics. As AI systems produce more mathematical claims, formal proof becomes the strongest available check. Benchmarks that test research-level statements assess whether that check is feasible.

• Education and training tools. Interactive proof assistants with AI assistance could help students and early-career researchers learn formalization, provided the prover handles non-toy statements.

• Software and hardware verification. Lean and similar assistants are used to verify systems code and cryptographic protocols. Provers that can handle project-scale, non-self-contained theorems translate directly to that setting.

Industry relevance. Formal verification of software, compilers, and cryptography depends on scaling proof engineering. Labs at DeepSeek, Google DeepMind, Microsoft Research, and elsewhere are training provers; RLMEval provides a benchmark that resists saturation and can be reissued annually with fresh projects, making it a useful neutral yardstick for comparing those efforts. The LeanInteract tooling is also independently useful to any team that needs programmatic access to Lean across versions.

Future Directions

• Better context retrieval. The current setup feeds the model only the in-file text preceding the theorem. Since real projects spread dependencies across many files, retrieval-augmented generation or automatic premise selection over the whole project — as is standard in software engineering — is the obvious next step.

• Lemma discovery and generation. The consistent easy-vs-normal gap shows models rely on human-provided auxiliary lemmas. Teaching models to conjecture and prove those intermediate results is a high-value research target.

• Making informal proofs usable. Many informal proofs in real blueprints are terse and refer to other results by shorthand, so they underperform their potential. Research into context-enriched or expanded informal proofs could unlock more of the autoformalization signal.

• Scaling and contamination control. The paper used a 7B model and pass@128 rather than the 671B model and pass@8192 used in prior work, so its numbers are likely a lower bound. Extending evaluation to larger budgets, larger models, and fresh projects released after model training cutoffs would both sharpen the estimate and reduce data-contamination risk.

• Annual versioning. The authors commit to releasing new RLMEval versions built from newer Lean projects, which raises the question of how to keep results comparable across versions.

Target Audience

Researchers in automated theorem proving, formal methods, and LLM reasoning; practitioners building proof assistants or AI proof-search tools; and mathematicians involved in or curious about Lean formalization projects. The paper is also relevant to anyone evaluating the gap between benchmark performance and real-world deployment of LLMs, since the core methodological point — that curated benchmarks overstate capability — generalizes beyond mathematics. Readers without prior exposure to Lean or proof assistants will need supplementary background to follow the technical details.

Authors’ abstract

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 Lean projects, reveals a significant gap: progress on existing benchmarks does not readily translate to these more realistic settings, with the best model achieving only a 10.3 % pass rate. RLMEval provides a new, challenging benchmark designed to guide and accelerate progress in automated reasoning for formal mathematics.