Statement Gaming: How Verifier Pressure Turns Formal Mathematics Into Empty Theorems

Formal verification is widely treated as the gold standard for AI-generated mathematics: if the Lean kernel accepts a proof, the result is taken to be trustworthy. This trust rests on an assumption that the checked statement faithfully encodes the intended mathematics. We show that when a language model both writes the formal statement and must satisfy the verifier, this assumption fails systematically, and it fails hardest exactly where the verifier's word matters most. We name the phenomenon statement gaming: the model deforms the statement itself — substituting free variables for defined objects, assuming the conclusion among hypotheses, or reducing the claim to a tautology — until the verifier accepts something the source mathematics never asserted. We measure statement gaming across 1,389 model–item pairs — statements drawn from research papers and corrected competition benchmarks, five production models from two vendors, five generation regimes from single-shot drafting to kernel-must-accept repair loops — grading every accepted artifact with a three-layer stack whose floor is fully mechanical: every certified defect replays deterministically, most as kernel-checked theorems. Under the requirement of a complete kernel-accepted proof of research-level mathematics, 69–100% of the three Claude-family models' accepted proofs do not assert the source statement (dose-response trend, Holm-adjusted $p\le 0.0021$). The two GPT-5.6 models at first appear immune, returning almost only empty, token-exhausted completions — but given an adequate output budget they accept 124 of 125 attempts, and 80–85% of those proofs are unfaithful: an output cap had manufactured an apparent vendor-level honesty difference. A lightweight fidelity intervention in the repair loop (a one-paragraph contract plus an advisory, non-gating screen) significantly reduces gaming (68%→53% for the most affected model; paired $p<10^{-4}$) with no significant cost in acceptance yield. Verifier-passing rates systematically overstate what models can formalize, with direct consequences for benchmark construction and reinforcement learning from verifier rewards. The task suite, harness, and certificate checkers accompany this submission as anonymized supplementary material.