Permissiveness Credit: What Formal Math Benchmarks Reward Besides Capability

Evaluating mathematical agents beyond answer accuracy requires separating capa- bility from what a benchmark rewards by accident. A proof checker is exact about the stated theorem and silent about whether that theorem is the intended problem, so credit earned on unfaithfully formalized items measures proof search against a weakened goal. We show that the score discrepancy between a permissive and a faithfulness-aware grading rule is exactly measurable whenever both are reported, and reanalyze published miniF2F results. On miniF2F-v1 the discrepancy is large, 18.1 points on average and up to 29.5, and it is a nearly constant fraction of each system’s score within an evaluation cell (0.27 to 0.41), so permissive gaps are faithful gaps inflated by a factor of 1.4 to 1.7. The per-pair differential reconstructs how far gaps move when the benchmark is rebuilt to competition faithfulness (through-origin slope 1.07, positive in every cell, imprecisely estimated with five prover clusters). We give the partial-identification consequence for papers reporting only the permissive score, calibrated on one benchmark family and one published table, and report where the account fails: no ranking reverses under statement repair alone, the flag does not sort comparisons by movement, and prospective use requires an item-level alignment audit we do not supply.