Formal proofs in Lean 4 that pass the type checker can vary widely in quality along dimensions valued by human mathematicians. As automated proof generation scales, evaluating these qualitative standards places a heavy burden on Mathlib reviewers.

ProofJudge is an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. The judge is grounded via tool access (querying Mathlib through bash) to the commit a PR is applied to. Alignment with human reviewers is measured by whether the judge rates the accepted post-revision version above the rejected pre-revision version.

Evaluated on 218 declaration pairs from distinct Mathlib PRs, all six judge models recovered reviewer preferences above chance, from 80.8% (claude-sonnet-5) to 63.5% (deepseek-v4-flash). Two open-weight judges reached roughly 70% at a tenth of the best judge's cost. Judges were noisy, with verdicts flipping across replicates.