Research map / Large language models / Agents, code and math

MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries

NeurIPS 2026 · Large language models › Agents, code and math · approach: Software engineering agents · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces MathlibPR, a benchmark of build-passing Mathlib4 PR snapshots labeled merge-ready vs not-merge-ready, and a three-stage protocol evaluating LLM models and coding agents on judging merge-readiness; finds none reliably distinguish the classes.

Problem

Whether LLMs can judge if build-passing Lean/Mathlib4 pull requests are merge-ready (follow conventions, fit the library), a review step that currently bottlenecks Mathlib growth and is not captured by kernel-based correctness checks.

Approach

Builds a benchmark from real Mathlib4 PR histories where all snapshots already compile, labels accepted versus revised-or-unmerged snapshots, and evaluates with staged context (diff and guidelines, then linter/import diagnostics, then PR title/description) plus read-only repository access for agents, using structured reviewer JSON with eight rubric axes.

Key results

• Best LLM-model Stage 3 balanced accuracy is 36.0% (DeepSeek); Qwen reaches 24.1%, Goedel and Kimina are lower.
• Codex reaches 92.0% MR recall at Stage 3 but only 12.0% NMR recall, giving 52.0% balanced accuracy.
• Within-PR pairwise accuracy for LLM models stays near chance (about 49-52% at Stage 3 for DeepSeek and Qwen).

Surprising findings

• Richer context (diagnostics, PR intent) and repository access do not close the gap; systems still fail to recognize not-merge-ready snapshots.
• Goedel and Kimina, trained for Lean theorem proving, mostly fail to produce the required JSON output (invalid rates of 86.5% and 88.7% at Stage 3).

Limitations

• Labels derive from historical maintainer decisions and may reflect non-technical factors such as timing or author abandonment.
• Agent evaluation uses a balanced 500/500 subset due to cost, limiting comparability with full-benchmark model results.
• Benchmark covers a selective slice of closed PRs constrained by recoverable build-check records.

Experimental setup

Datasets: Mathlib4 closed PR histories

Benchmarks: MathlibPR

Metrics: MR recall NMR recall balanced accuracy valid-output rate AUROC within-PR pairwise accuracy

Baselines: DeepSeek-R1-Distill-Qwen Qwen3-8B Goedel-Prover-V2-32B Kimina-Prover-Distill-8B Codex Claude Code

Builds on: LeanDojo CodeReviewer SWE-bench

Closest papers by meaning

• MathArena: Evaluating LLMs on Uncontaminated Math Competitions (NeurIPS 2025 · similarity 0.86)
• DAG-Math: Graph-Guided Mathematical Reasoning in LLMs (ICLR 2026 · similarity 0.86)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.85)
• MathCoder: Seamless Code Integration in LLMs for Enhanced Mathematical Reasoning (ICLR 2024 · similarity 0.85)
• RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.85)
• OpenMathInstruct-2: Accelerating AI for Math with Massive Open-Source Instruction Data (ICLR 2025 · similarity 0.85)