Summary of "ProofJudge: Tool-Grounded LLM Evaluation of Formal Proof Quality in Mathlib"

Summary (Overview)

• ProofJudge is an agentic LLM-as-judge system that evaluates formal proof quality in Lean 4 beyond mere correctness, scoring along five dimensions: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions.
• The system is evaluated on a novel dataset of 218 declaration pairs drawn from distinct Mathlib pull requests, where each pair contains an initial (rejected) and final (accepted) revision.
• The judge agent is grounded by tool access to the actual library state at the commit where the PR was applied, enabling it to search and query Mathlib as a human reviewer would.
• All six judge models recover human reviewer preferences well above chance, ranging from 80.8% (claude-sonnet-5) to 63.5% (deepseek-v4-flash), all with $p < 10^{-5}$ by sign test.
• Two open-weight judges (muse-glimmer-30b and inkling-small) achieve ~70% alignment at roughly a tenth of the cost of the best closed-weight judge.

Introduction and Theoretical Foundation

The paper addresses a critical gap in the formal verification ecosystem: while the Lean 4 kernel guarantees that proofs passing the type checker are provably correct, correctness alone does not capture what makes formal proofs valuable to mathematicians.

Key Motivations:

• The rise of reinforcement learning from verifiable reward has made Lean 4 an attractive verifier for LLM-generated proofs, increasing both human-collaborative[4] and autonomous[3] proof writing.
• Critics argue the value of formalization lies not in verifying statements but in "building libraries and infrastructure to support future work" — i.e., the quality and reusability of the proofs themselves[1].
• Mathlib enforces quality standards through human code review, evaluating tactic hygiene, generality of lemma statements, proof structure, naming conventions, and whether proofs decompose into independently reusable components.
• Current LLM-generated proofs frequently violate these deeper structural and stylistic properties[5], creating a heavy burden on skilled Mathlib reviewers as the cost of generating valid proofs decreases.

The theoretical foundation rests on the observation that quality dimensions beyond correctness are legible to language model agents — a claim the paper empirically validates.

Methodology

2.1 Rubric Design

ProofJudge decomposes the verdict into five independently scored dimensions (each on a 1–10 scale):

1. Library leverage — whether the proof reuses existing Mathlib declarations rather than reconstructing them
2. Automation fit — how well the proof aligns with Lean's automation tools (e.g., simp, omega)
3. Structural clarity — whether the proof decomposes into understandable, independently reusable components
4. Statement quality — generality and naming of lemma statements
5. Mathlib conventions — adherence to library-specific stylistic norms

The harness weights these five scores toward a final verdict. This rubric is based on Mathlib's review norms, distinguishing ProofJudge from prior work on semantic correctness of PRs[6].

2.2 Dataset Construction

• Dataset: 218 declaration pairs from Mathlib pull requests, where each pair contains an early (rejected) and final (accepted) revision.
• Construction method: claude-sonnet-5 reviewed past PRs to identify those with significant differences between earliest and final revisions, excluding changes that were purely linting or involved new declarations.
• Splits: Dev split of 123 pairs (used to tune the rubric) and a test split of 218 pairs (used for evaluation).
• Evaluation protocol: Each judge scores both revisions independently, unaware of the other revision's score or that a paired comparison is being made. Judges are limited to 20 tool calls before being forced to make a determination.

Empirical Validation / Results

Table 1: Judge Performance on the 218-Pair Test Split

Intervals are a clustered bootstrap over declarations and replicates. Cost is published list rates times token counts.

Key Findings:

• Every judge recovers reviewer preferences far above the 50% random-chance baseline.
• Cost-performance tradeoff: The best judge (claude-sonnet-5) achieves 80.8% at $1.392/pair, while open-weight judges achieve ~70% at roughly one-tenth the cost.
• Judge noise is substantial: Re-running a judge over the same declarations flips between a fifth and nearly half of its verdicts. A single run's interval hides this badly — the same ablation returns $p = 0.34$ on one replicate and $p = 0.006$ on another, meaning single-run benchmarks would report differences that replication does not support.

3.1 Example Grading (PR 11640)

In a representative example, the initial proof of Set.restrictPreimage_isClosedMap reconstructed a result Mathlib already provided. The merged revision replaces it in one line:

H.restrictPreimage s

The judge agent searched the repository for the existing declaration, quoted the signature it found, and marked the initial PR down on library leverage. Every judge reduced the score of the initial PR in every rollout. This demonstrates that:

"While this would not be possible with regular expressions or linting, an agent with tool access can search the library, understand the semantic meaning of what it finds, and act as a reviewer would."

Theoretical and Practical Implications

Theoretical Implications:

• The results establish that qualitative properties of formal proofs (beyond correctness) are legible to language model agents, contradicting the assumption that these judgments require deep human mathematical intuition.
• The tool-grounded approach demonstrates the value of agentic judges over static ones: the ability to query the library state enables semantic understanding (e.g., recognizing that a result already exists) that pure text-based analysis cannot achieve.

Practical Implications:

• Maintainer relief: The signal from ProofJudge could be used to reduce the burden on Mathlib maintainers by pre-filtering or pre-screening PRs.
• Iterative improvement: A reliable judge gives models a signal to iterate a PR against, improving quality before a human reviewer sees it.
• Cost accessibility: Open-weight judges at ~70% alignment and $0.13/pair make this approach accessible to the broader research community.
• The noise caveat: The high variance across replicates means that single-run evaluations are unreliable — a critical warning for anyone building on this methodology.

Conclusion

The paper concludes that correctness is not the only property of formal proof that matters. Mathematicians value understandability and library contributions that enable future work. The alignment scores demonstrate that these qualities are not illegible to language model agents, establishing that this signal can be used to relieve maintainer burden and create agents capable of writing Lean 4 PRs that maintainers would welcome.

Future Work Directions

1. Cost reduction and open-sourcing: Develop judges that perform at claude-sonnet-5's level but cheaper and open-source.
2. Noise reduction via two approaches:
   • Splitting the rubric into five single-dimension judges so each makes more focused use of tools.
   • Treating the tool-call budget itself as a tunable parameter.
3. Reinforcement learning: Using ProofJudge results as a reward signal to train models that write better proofs before human review.