MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries
For the Lean/Mathlib community, this benchmark provides a first step toward automated reviewer assistants and reward models to help evaluate PRs and guide LLMs to produce merge-ready contributions.
The paper introduces MathlibPR, a benchmark for evaluating LLMs' ability to assess whether pull requests to the Mathlib formal mathematics library are merge-ready. Experiments show that both LLM models and agents struggle to distinguish merge-ready PRs from those that pass builds but are not merged, highlighting a bottleneck in the review process.
The ecosystem of Lean and Mathlib has become the de facto standard for large language model (LLM) assisted formal reasoning with remarkable successes in recent years. Those successes, however, only consume Mathlib as an essential dependency but do not directly contribute to it. In the meantime, the growth of Mathlib has recently been bottlenecked by the review process, which requires human reviewers to judge whether proposed pull requests (PRs) follow the Mathlib's conventions and are worth integrating as part of a shared mathematical infrastructure. This leads to our central question: can LLMs help review Mathlib PRs? To this end, we introduce MathlibPR, a benchmark built from real Mathlib4 PR histories. We further propose a staged evaluation protocol and use it to evaluate both LLM models (e.g., DeepSeek, Qwen, Goedel, and Kimina) and LLM agents (e.g., Codex and Claude Code). Surprisingly, both LLM models and LLM agents struggle to distinguish merge-ready PRs from build-passing PRs that were revised or never merged. By turning Mathlib PR histories into a supervised signal, MathlibPR provides a step toward reviewer assistants and reward models that could help evaluate PRs and steer LLMs toward producing merge-ready Mathlib contributions.