PocketLean: A Lightweight Mathlib Retriever for Proof Agents

We present PocketLean, a lightweight Mathlib retriever for proof agents that learns from their own retrieval calls. Agents query Mathlib, a large library that changes across versions, repeatedly as they write, check, and revise, so retrieval must be cheap to run and to re-index. Pairing each recorded call with the lemmas its Lean-checked final proof uses yields query-level weak supervision. After multi-source query training, R${}^2$Evo (Replay-to-Rollout Evolution) applies this supervision over generations, first on recorded trajectories and then on rollouts collected with the updated retriever, so that the supervision follows the queries each update elicits. We also introduce ProofCall, a benchmark of 1,999 recorded agent calls in five sets, each labeled with the proof-used lemmas judged relevant to it, complementing the static queries of the public Lean Finder benchmark. Agents not told how to phrase their queries mostly issue approximate formal statements rather than natural-language questions, the form on which PocketLean is strongest. The 0.6B PocketLean reaches 78.9% mean Recall@10 on the Lean Finder benchmark against 77.9% for the 7B Lean Finder model, and the highest hit@10 on all five ProofCall sets, 4.3 to 7.6 points above the strongest external system. In end-to-end proving on subsets we curate from miniF2F and ProofNet, it more than doubles the success rate without retrieval, scores highest among the evaluated retrievers, and cuts the prover's tokens per model call by 36%. It needs only a single encoder and a per-version Mathlib index, and on a CPU it encodes 15 times as many queries per second as Lean Finder; we will release the weights, code, and data.