mlsanityData to 14 Oct 2026

RLMEval: Evaluating Research-Level Neural Theorem Proving

arXiv 2510.25427 ↗First posted 29 Oct 2025cs.CL cs.AIcited by 8

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. Cited by 8 papers in the map (data through 14 Oct 2026). Builds on 11 of its 18 references that are in the map. First posted on arXiv 29 Oct 2025.

Builds on

11 of 18 references.

References · 11

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  3. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  5. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  6. 2022Autoformalization with Large Language Modelscited by 263
  7. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  8. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  9. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 37
  10. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 35
  11. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 18

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 8.

8 papers.

  1. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 8
  2. 2026SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalizationcited by 4
  3. 2026Evaluation of LLMs for Mathematical Formalization in Leancited by 3
  4. 2026LeanFlow: A Case Study in Workflow-Driven Lean Autoformalizationcited by 3
  5. 2026Automating Formal Verification with Reinforcement Learning and Recursive Inferencecited by 1
  6. 2026CAM-Bench: A Benchmark for Computational and Applied Mathematics in Leancited by 0
  7. 2026Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Provingcited by 0
  8. 2026Beyond LLM Judge: Mechanical Verification for Agentic Autoformalizationcited by 0