What Helps Agentic Lean Provers? A Trace-Level Attribution Study

Agentic Lean provers now do much more than sample a proof: they compile candidates, read errors, inspect proof states, query libraries, retrieve premises, and decide whether to keep searching or submit. That makes pass rate hard to interpret. We study this attribution problem with trace-level ablations on a frozen 100-task Lean~4 benchmark. The clearest aggregate lesson is simple: compiler feedback helps: M1@8 solves $5$--$8/100$ tasks across four Gemini runs, compared with $0/100$ for one-shot generation and $3/100$ for BoN@8. Residual proof-state feedback is useful but mixed. Richer tool and retrieval channels do not automatically become better provers; they mostly change the route through a problem: what the agent looks up, what it cites, which tasks it reaches, how it spends tool calls, and whether it ever commits. These traces expose a recurring failure mode: many unsuccessful runs keep probing instead of turning available evidence into a final checked proof. We argue that this is exactly what lower-rung ablations should reveal: when an agent should retrieve, search, restart, decompose, or commit.