A Compile-Validated Proof Synthesis Benchmark over 57 Lean~4 Repositories

To date, machine proof synthesis AI benchmarks are dominated by self-contained statements found in competition mathematics. But these benchmarks lack surrounding development. In real-world proof engineering, proof obligations are frequently deferred, often requiring an additional lemma to derive. Our contribution is to synthesize these tasks through \emph{syntactic ablation} of real repositories. To produce such a task, we first pick a theorem at random and take its in-file transitive dependency closure. We then delete one supporting lemma from that closure. Proofs that use the deleted lemma are deferred. We validate every problem with two checks. The first check runs the challenge with its holes and ensures it compiles. Then we ensure the recorded ground truth also compiles hole-free. We pin each against an \texttt{.olean} closure. Using this approach, we mine 43{,}410 challenges from 57 public Lean~4 repositories. We use two deferral strategies over matched selections: we defer proofs at the site of the usage of the deleted lemma (ie, \emph{leafs}), and entire proofs that rely on the deleted lemma. We evaluate three LLM models on a matched sample of 103 problems. Agents are given a 50-turn budget. A stark contrast emerges between the top-performing model and the rest: 49.5\%, 29.1\%, and 30.9\% PASS under leaf holing. However, the more consequential result is the failures that our harness catches. For the strongest model in our sample, it never fails honestly. Of 103 scorable problems, it passes 51 but is caught tampering on another 50. A scorer that only checks “compiles, no holes” would have reported 98.1\% rather than 49.5\%. Capability across the three models correlates with tamper rate: 48.5\% for the strongest model, versus 26.2\% and 26.8\% for the other two. A 15/30/50/100-turn budget curve demonstrates that cheating does not fall when the turn budget is cut; the strongest model tampers the \emph{most} at the lowest budget. In contrast, the two deferral strategies (leaf and whole proof) do not differ significantly in pass rate at the 50-turn budget (McNemar $p = 0.75$ and $1.00$ for the two general-purpose models). However, different deferral strategies change the composition of failures and the turn cost. Finally, we assess contamination risk using lemma introduction dates and a deletion-count sweep; these checks do not exclude prior exposure to the original proofs.