RLME val: Evaluating Research-Level Neural Theorem Proving (2025)

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.

## introduction automatically translating mathematical content from natural language into a formal language suitable for proof assistants @xcite , is crucial for bridging human mathematical reasoning with machine-verifiable proofs. neural theorem proving (ntp) and proof autoformalization using large language models (llms) have demonstrated remarkable progress @xcite in these tasks. this success is predominantly measured on curated benchmarks such as minif2f @xcite or proofnet @xcite . while valuable, these benchmarks suffer from issues, such as saturation (e.g., minif2f reaching 88.9 % success @xcite ), formalization inaccuracies (e.g., ∼30 % in proofnet @xcite ), or a narrow focus on competition-style problems. they do not fully capture the complexities of realworld, research-level mathematics. consequently, model performance on these benchmarks may not reliably predict their practical utility in assisting with ongoing, complex formalization projects. to address this gap, this work introduces rlmeval foot_0 , a benchmark for evaluating neural theorem proving and proof autoformalization on research-level mathematics within contemporary lean 4 projects. rlmeval distinguishes itself by focusing on blueprint theorems, significant, highlevel results from real-world lean projects. these theorems embody core conceptual advances, unlike the more numerous auxiliary lemmas which often involve smaller, routine deductions and typically constitute over 75% of theorems in lean projects (see ## related work research in neural theorem proving (ntp) has seen significant advancements, from early work like gpt-f @xcite to recent llm-based techniques (e.g., @xcite @xcite . some methods explore using intermediate, possibly less-rigorous reasoning to guide formal proof generation, while others, like leanagent @xcite , train on multiple lean repositories in a curriculum to accumulate knowledge. proof autoformalization has also progressed, with early breakthroughs in isabelle where models like codex translated informal math problems into formal specifications @xcite . the draft, sketch, and prove (dsp) approach @xcite further improved this by using informal proofs to generate formal proof sketches, which are then completed by an automated theorem prover. minif2f @xcite offers olympiadlevel problems across multiple proof assistants. proofnet @xcite provides lean theorems with informal statements/proofs, targeting both autoformalization and theorem proving. putnambench @xcite focuses on challenging putnam competition problems. these benchmarks are focused on competitionstyle problems or undergraduate-level mathematics. minictx @xcite evaluates provers on real lean projects but is tied to a specific lean version and includes all theorems, many of which are auxiliary technical lemmas. rlmeval differentiates itself by: (1) focusing on research-level mathematics drawn from real-world lean blueprint projects @xcite ; (2) specifically targeting blueprint theorems, which represent significant conceptual steps, unlike benchmarks that include numerous simpler lemmas (see ## methodology rlmeval provides a comprehensive suite for evaluating neural theorem proving and proof autoformalization on research-level lean mathematics. we release it along with a dedicated python interface, leaninteract, for robust communication with the lean proof assistant (moura and ullrich, 2021), offering programmatic control over lean through its repl interface @xcite . a key feature crucial for rlmeval is its multi-version support, achieved through manual backporting of the latest repl features and bug fixes to all 41 lean versions between v4.7.0-rc1 and v4.19.0 (a significant undertaking ensuring broad applicability). this approach prioritizes broad compatibility and ease of use for benchmarking across the evolving lean ecosystem, setting it apart from existing interaction tools like leandojo @xcite or pantograph @xcite , which are tied to specific lean versions or require compute-intensive project tracing. this property is a key cornerstone of rlmeval for its extensibility, laying the foundations for longterm maintenance and future updates. because our benchmark is based on real-world projects, data contamination concerns apply. in order to continuously mitigate this risks, we plan to release new versions of rlmeval with more recent lean projects to continuously reduce data contamination risks when evaluating current and future models. benchmark design. our methodology for curating rlmeval is inspired by rlm25 @xcite , a research-level benchmark for autoformalization of theorem statements. rlmeval leverages existing lean blueprint projects (massot, 2025), which curate high-quality alignments between natural language mathematics and their formal counterparts. these projects, authored by domain experts, ensure the precision and real-world relevance of the benchmark data. a core design principle of rlmeval is its focus on blueprint theorems, i.e. formal theorems that are linked in the informal blueprint of the projects. the blueprint theorems represent the main, high-level steps of mathematical development, akin to theorems found in research papers. this contrasts with previous works @xcite that include a large proportion of simpler, auxiliary lemmas. to assess models under varying conditions, rlmeval uses two evaluation modes: ## experimental setup and results we evaluate several llms on the rlmeval tasks. our primary metric is pass@k, which measures the percentage of problems solved with at least one successful proof among k generated attempts. for our main results, we use @xmath0, a budget significantly larger than the 8 samples used in minictx @xcite , allowing for a more comprehensive assessment. for each theorem, models receive the full in-file context up to the point where the proof is to be generated, including all preceding definitions, lemmas, and imports within that specific file. in normal mode, lemmas not present in the informal blueprint are excluded from the context, while in easy mode, all lemmas from the project are available. our baseline model is llemma 7b @xcite , a model pretrained on mathematics, but not for proof-search specifically. we also evaluate leading models specifically tuned for lean theorem proving: deepseek-prover-v1.5-rl @xcite , deepseek-prover-v2-7b @xcite , goedel-prover-sft @xcite , and kiminaprover-preview-7b @xcite . our evaluation on rlmeval examines their ability to generalize to research-level mathematics. l l e m m a -7 b d e e p s e e k -p r o v e r -v 1 . 5 -r l d e e p s e e k -p r o v e r -v 2 -7 b g o e d e l -p r o v e r -s f t k i m i n a p r o v e r -7 b 0 5 10 15 20 9.5 11.4 14.7 7.0 4.1 4.8 6.9 8.8 4.7 3.2 pass rate (%) neural theorem proving easy normal l l e m m a -7 b d e e p s e e k -p r o v e r -v 1 . 5 -r l d e e p s e e k -p r o v e r -v 2 -7 b g o e d e l -p r o v e r -s f t k i m i n a p r o v e r -7 b 0 5 10 15 20 7.6 12.2 16.7 6.4 3.6 5.6 7.3 10.3 4.9 4.2 pass rate (%) proof autoformalization easy normal figure 1: pass rate on rlmeval using pass@128 for neural theorem proving (left) and proof autoformalization (right), in easy and normal modes. a smaller pass@32 budget. this disparity underscores that current models struggle significantly with the complexity of research-level mathematics in real-world projects. models consistently perform better in the "easy" mode (with access to project-specific auxiliary lemmas). deepseek-prover-v2-7b improves from 8.8 % (normal) to 14.7 % (easy) in neural theorem proving (ntp), and from 10.3 % to 16.7 % in proof autoformalization. this performance gap highlights the challenges models face when working without direct access to project-specific lemma support. providing an informal proof offers a modest benefit (proof autoformalization versus neural theorem proving (ntp)). for deepseek-prover-v2-7b (normal mode), this translates to an improvement of ∼1.5 percentage points (from 8.8 % to 10.3 %). this suggests that current models can leverage informal proofs to some extent, but the benefit remains limited for complex, research-level problems. performance varies substantially across rlmeval projects (see figure 2 illustrates how performance scales with an increasing number of samples per theorem for various models. as in traditional benchmarks, we observe that pass rate improves with additional samples. while pass rates continue to increase with more samples for most models, the gains diminish noticeably, suggesting that simply scaling up sampling may not overcome the fundamental challenges posed by research-level mathematics. this contrasts with results on benchmarks like minif2f, where aggressive sampling (e.g., pass@8192) produced substantial improvements @xcite , further highlighting the greater difficulty of rlmeval. ## conclusion we introduced rlmeval, a benchmark for neural theorem proving and proof autoformalization on research-level mathematics. focusing on real-world mathematical formalization challenges, rlmeval establishes a realistic standard for evaluating the practical utility of neural theorem provers in mathematical settings. our evaluation on 613 research-level mathematics theorems reveals a stark performance drop compared to traditional benchmarks like minif2f. the best model achieved only 10.3 % on proof autoformalization (normal mode), highlighting that current models are still far from reliably handling the complexities of ongoing formalization efforts. this performance gap is par-ticularly pronounced for projects like carleson with complex mathematical structures, while being somewhat narrower for more concrete domains like algebraic number theory (flt3). the disparity between "easy" and "normal" modes across all models demonstrates the critical role of auxiliary lemmas in successful theorem proving. access to these intermediate results improved performance by up to 6%, suggesting that enhanced techniques for lemma discovery or generation could be valuable directions for future research.