Beyond Solve Rates: Harness Effects and Run-to-Run Variability in Agentic Theorem Proving

Evaluations of theorem-proving systems typically summarise a complete nondeterministic system by one benchmark solve rate. We compare runs problem by problem using their discordance: the problems solved in only one of two runs. Discordance estimates run-to-run variability, supports exact paired tests between designs, and shows whether gains are concentrated on a few problems or distributed across many. We also decompose harness differences into retrieval, scratch-compilation, subagent, and memory tools available to a fixed Lean agent, evaluated on 90 FATE-X problems. Replicate scores differ by about two problems on average, but the runs disagree on six to eleven individual problems. Text search over Mathlib gains 8 problems over the baseline and reaches its \\$1 score at \\$0.50.