Elamur Research⌕
☰
home / papers / 2025 / RLMEval: Evaluating Research-Level Neural Theorem Proving

RLMEval: Evaluating Research-Level Neural Theorem Proving

Paper · 2025 · Auguste Poiroux, Antoine Bosselut and Viktor Kunčak

Summary

LLM-based provers score well on curated benchmarks such as MiniF2F and ProofNet. Those benchmarks, however, are close to saturation, contain formalization errors, or focus on competition-style problems. As a result, they say little about whether models can help with real formalization work. The authors introduce RLMEval, a benchmark built from six Lean 4 blueprint projects written by domain experts. It contains only blueprint theorems, meaning the major results linked to the informal blueprint, and leaves out the many routine auxiliary lemmas.

RLMEval covers two tasks:

  • Neural theorem proving: produce a proof from a formal statement.
  • Proof autoformalization: produce a formal proof from a statement plus an informal proof.

Each task runs in two settings. In the "easy" setting, the model can use the project's auxiliary lemmas. In the "normal" setting, those lemmas are hidden.

The release includes LeanInteract, a Python interface that works with many Lean versions. This makes the benchmark extensible, and the authors plan yearly versions to limit data contamination.

Five open models were tested at pass@128, and all performed poorly. The best reached roughly 10% in the realistic setting, which shows that strong results on existing benchmarks do not carry over to research-level mathematics.

Key points

  • Benchmark contents: RLMEval has 613 theorems from Carleson, FLT, PFR, PNT, FLT3 and TLB, spanning analysis, number theory, combinatorics, and information/probability theory. It is released under Apache 2.0.
  • Difficulty of blueprint theorems: Their proofs average 16.6 lines, compared with 6.6 lines for auxiliary lemmas. Auxiliary lemmas often make up more than 75% of a project's theorems.
  • Best model results: DeepSeek-Prover-V2-7B performed best.
    • Proof autoformalization: 10.3% (normal) and 16.7% (easy).
    • Theorem proving: 8.8% (normal) and 14.7% (easy).
    • For comparison, it reports above 75% on MiniF2F.
  • Other models evaluated: Llemma 7B (baseline), DeepSeek-Prover-V1.5-RL, Goedel-Prover-SFT, and Kimina-Prover-Preview-7B.
  • LeanInteract: The tool backports REPL features to all 41 Lean versions from v4.7.0-rc1 to v4.19.0. Informal proofs gave only a small gain (about 1.5 points), partly because many are terse and depend on project context.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓École Polytechnique Fédérale de LausanneLausanne · Switzerland56 works · 8,189 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Auguste Poiroux, Antoine Bosselut and Viktor Kunčak. 2025. RLMEval: Evaluating Research-Level Neural Theorem Proving. Findings of the Association for Computational Linguistics: EMNLP 2025.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2025.findings-emnlp.581 · arXiv 2510.25427

@inproceedings{poiroux2025rlmeval,
  title = {{RLMEval: Evaluating Research-Level Neural Theorem Proving}},
  author = {Auguste Poiroux, Antoine Bosselut and Viktor Kunčak},
  booktitle = {Findings of the Association for Computational Linguistics: EMNLP 2025},
  year = {2025},
  doi = {10.18653/v1/2025.findings-emnlp.581},
  eprint = {2510.25427},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2025.findings-emnlp.581}
}

References

8 references, 4 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. arXiv preprint. ArXiv:2009.03393 [cs, stat].
  2. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. 2024. Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4. arXiv preprint. ArXiv:2410.16429.
  3. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023a. find
  4. ProofNet: Autoformalizing Auguste Poiroux, Viktor Kuncak, and Antoine Bosselut. 2025. LeanInteract: A Python Interface for Lean 4. Original-date: 2025-02-05T21:35:17Z. find
  5. Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. 2024. Improving Autoformalization using Type Checking. arXiv preprint. ArXiv:2406.07222 [cs]. find
  6. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. 2025. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinfo…
  7. Christian Szegedy. 2020. A Promising Path Towards Autoformalization and General Artificial Intelligence. volume 12236, pages 3–20, Cham. Springer International Publishing. Book Title: Intelligent Computer Mathematics Series Title: Lecture Notes in Computer Science. find
  8. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. 2024. Putnam-Bench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. arXiv preprint. ArXiv:2407.11214.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/poiroux-2025-rlmeval-evaluating-research-level-neural/