ai4math 
Kill the tail, not the cores: profiling the verifier under RL-with-verifiers
As RL-with-verifiers scales, the Lean verifier is both the reward source and the throughput bottleneck — a CPU/scheduling problem almost nobody benchmarks on commodity, on-prem hardware. We profiled it: on an 8-core box, ~4.5% of proofs run away and eat most of the single-thread wall, and a tuned per-proof deadline beats adding cores. The honest-measurer story (including the claim we had to retract) is the point.