# Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

arXiv: https://arxiv.org/abs/2605.10379 · HTML: https://mlsanity.com/paper/2605.10379/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 44 of its 55 references that are in the map.
- First posted on arXiv 11 May 2026.

## Builds on (most cited first, 30 of 44)

- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [gpt-oss-120b & gpt-oss-20b Model Card](https://mlsanity.com/paper/2508.10925/) (2025)
- [DeepSeek-V3.2: Pushing the Frontier of Open Large Language Models](https://mlsanity.com/paper/2512.02556/) (2025)
- [GLM-5: from Vibe Coding to Agentic Engineering](https://mlsanity.com/paper/2602.15763/) (2026)
- [Kimi K2.5: Visual Agentic Intelligence](https://mlsanity.com/paper/2602.02276/) (2026)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Justice or Prejudice? Quantifying Biases in LLM-as-a-Judge](https://mlsanity.com/paper/2410.02736/) (2024)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [Judging the Judges: A Systematic Study of Position Bias in LLM-as-a-Judge](https://mlsanity.com/paper/2406.07791/) (2024)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [Self-Preference Bias in LLM-as-a-Judge](https://mlsanity.com/paper/2410.21819/) (2024)
- [WildBench: Benchmarking LLMs with Challenging Tasks from Real Users in the Wild](https://mlsanity.com/paper/2406.04770/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [AbstentionBench: Reasoning LLMs Fail on Unanswerable Questions](https://mlsanity.com/paper/2506.09038/) (2025)
- [Verbosity Bias in Preference Labeling by Large Language Models](https://mlsanity.com/paper/2310.10076/) (2023)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [Evaluating Language Models for Mathematics through Interactions](https://mlsanity.com/paper/2306.01694/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Step 3.5 Flash: Open Frontier-Level Intelligence with 11B Active Parameters](https://mlsanity.com/paper/2602.10604/) (2026)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMs](https://mlsanity.com/paper/2510.04721/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematics](https://mlsanity.com/paper/2504.01995/) (2025)
- [Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math](https://mlsanity.com/paper/2510.13744/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models](https://mlsanity.com/paper/2506.17114/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)

## Built on by (most cited first, 3 of 3)

- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics](https://mlsanity.com/paper/2606.29894/) (2026)
- [AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification](https://mlsanity.com/paper/2607.11849/) (2026)

## Abstract (arXiv)

Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient: mathematical proofs should also be clear, concise, insightful, and transferable to other problems. While this proof quality is subjective and depends on the reader and context, many of its components are concrete and broadly valued. In this work, we identify such components and introduce ProofRank, a benchmark curated from challenging mathematical competitions. ProofRank evaluates several scalable proxies of proof quality: (i) conciseness, measuring whether proofs avoid unnecessary steps; (ii) computational ease, measuring the extent to which a proof relies on tedious calculations; (iii) cognitive simplicity, measuring how accessible the used proof techniques are; (iv) diversity, measuring how varied a model's proofs for a single problem are; and (v) adaptivity, measuring whether a model can follow a specified proof technique. Across models, we find substantial differences in proof quality that are not captured by correctness-only benchmarks. We also observe significant trade-offs between proof-quality metrics and correctness, suggesting that future evaluations of mathematical reasoning should measure how useful LLM-generated proofs are.