RLMEval: Evaluating Research-Level Neural Theorem Proving
Auguste Poiroux, Antoine Bosselut, Viktor Kunčak · 2025
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-ofthe-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.