Beyond Aggregate Accuracy: Shared Failures and Context Sensitivity in Lean Proof Completion

Reliable mathematical assistants must produce machine-checked proofs even when the underlying argument is routine. We present LeanNumBench, a diagnostic benchmark of 160 numerical-analysis proof-completion tasks in Lean 4. Models receive fixed theorem statements and local declarations and generate proof bodies without interactive Lean feedback. Across five hosted endpoints, the best raw score is 145/160, rising to 148/160 with deterministic repair. Even after repair, at least three endpoints fail on each of 11 tasks. A separate evaluation shows that two endpoints with identical 150/160 scores share only 143 successes. Paired prompt comparisons record different outcomes with and without declaration context; checker-level analysis identifies recurring failures in tactic composition. These are single-response observations, not estimates of stable differences in model capabilities. They show why aggregate accuracy alone is insufficient for evaluating formal mathematical assistants and provide task-level targets for future interactive systems.