Methodology

The point of this site is that its numbers are comparable to one another. That only holds because of the choices on this page, and it stops holding wherever a caveat below says so.

What is held constant

One corpus: Every system indexes mathlib-4280 at revision c5f07cc71d42, pinned so a silent upstream re-upload cannot move a number.
Somebody else's benchmark: The evaluation set is MathlibQR from the LeanSearch v2 release, used byte-for-byte: the copy under harness/benchmarks/ hashes to 0ce093ebb9da, equal to upstream. We wrote none of the queries and dropped none of them, which is what makes these numbers comparable to that paper’s Table 1 rather than to a set we curated in our own favour.
One document renderer: Every model embeds byte-identical document text, produced by the lsv2-compat renderer (5f1e87b6661e). The hash is part of the vector path, so editing the renderer invalidates vectors instead of quietly mixing two encodings.
Exact search: Ranking is a full inner product over L2-normalized vectors, then a partial sort — no HNSW, no IVF, no approximation. An approximate index would add a recall error of its own on top of the model’s, and the two would be impossible to separate.
Query-side instructions only: The instruction-aware models take Instruct: …\nQuery: … on the query and nothing on the document, which is what their model cards specify. Applying it to documents changes the numbers and is asserted against in the harness tests.

How each metric is computed

Every figure on this site is one of the formulas below, macro-averaged over queries. They are transcriptions of harness/legendre_search/eval/curves.py rather than of a textbook: three of them embed a convention that is a choice, and a reader comparing our number to a paper’s needs the version we actually computed.

Ranked list: A system answers query q with d₁ … d_m, truncated at k_max = 200. Every metric here is therefore truncated too, so R@k_max is a lower bound on true recall — and comparing curves computed at two different k_max is invalid, which is why it is pinned in the manifest. A row whose service returns fewer results carries a k≤N badge and its metrics are undefined above N, not flat.
Gold units G: What counts as a right answer, as a set of sets. On theorem search G holds one unit: every corpus row the gold full_name resolved to, since a declaration can appear more than once in the export and any copy is correct. On premise selection it holds one unit per premise group, matching the source benchmark’s own semantics. So |G| is 1 on MathlibQR and the number of groups on MathlibMPR.
Position pos(g): The rank of the earliest retrieved member of unit g, or ∞ if none was retrieved. Ranks are 1-indexed, and a row returned twice counts at its first occurrence only — a backend must not be able to improve its score by repeating itself.
Hit count h(k): $h (k) = | {g \in G : pos (g) \leq k} |$
Both R@k and P@k are this over a different denominator, which is what makes them mutually consistent at group level.

Recall@k

curve on Compare · sparkline and R@10 column on the leaderboard

R @ k = \frac{h (k)}{| G |}

The fraction of gold units found within k. On theorem search |G| = 1, so it is simply whether the right declaration is in the top k, averaged over queries — which is also why its curve is a step function per query and only smooth once averaged.

Precision@k

curve on Compare, multi-relevant tasks only

P @ k = \frac{h (k)}{k}

Divides by k, not by the number of results returned. A system that returns 12 results for k=50 scores h(50)/50. That is the standard definition and it matters here because BM25 truncates at zero score while a dense system always fills k; n_retrieved is stored per query so the other convention remains computable. Group-level on premise selection: two groups covered inside five results is 2/5, counting distinct groups rather than raw document hits.

nDCG@k

curve on Compare · nDCG@10 is the leaderboard's default sort

nDCG @ k = \frac{DCG @ k}{IDCG @ k}

DCG @ k = \sum_{g \in G, pos (g) \leq k} \frac{1}{\log_{2} (pos (g) + 1)}

IDCG @ k = \sum_{i = 1}^{\min (k, | G |)} \frac{1}{\log_{2} (i + 1)}

Binary relevance, and IDCG is capped at min(k, |G|). The cap is the whole subtlety: the ideal ranking has only as many relevant documents as exist, so its gain stops accruing at k = |G| while DCG keeps growing until the last unit is found. Without it a single-gold query’s curve would divide by an ever-growing ideal and decay toward zero as k grew — the shape of a bug, not of a retrieval result. With |G| = 1 the whole expression reduces to 1/log₂(pos + 1), exactly the vendored implementation, and a harness test pins that reduction at every k so our figures stay citable against the published table.

MRR

leaderboard column

RR = \frac{1}{\min_{g \in G} pos (g)} (0 if nothing was found)

Only the first hit counts, so MRR is the metric most sensitive to the top of the list and the least sensitive to everything below it. A query with no gold unit retrieved contributes 0 rather than being dropped.

MAP

scalar summary of the PR curve

AP = \frac{1}{| G |} \sum_{j = 1}^{h (k_{max})} \frac{j}{p_{j}}

p₁ < … < p_j are the gold positions that were found, ascending, so j / p_j is the precision at the moment the j-th unit appeared. Divides by |G|, not by the number of hits. Gold that was never retrieved therefore costs you, which is what makes MAP a stricter summary than R@k rather than a rescaling of it.

Covered@k

premise selection (MathlibMPR)

Covered @ k = [h (k) = | G |]

The bracket is 1 when every gold unit is inside the top k and 0 otherwise, averaged over queries. A proof needs all of its premises, so partial recall is not a partial success — this is the metric that says so. It can never exceed R@k, and equals it only when no query is partially covered.

PR curve

multi-relevant tasks

P_{interp} (r) = \max_{k : R @ k \geq r} P @ k, r \in {0, 0.1, \dots, 1}

Interpolated precision at the 11 conventional recall levels, and 0 where a level is unreachable rather than the last known precision carried forward. Interpolation is what makes PR curves comparable across queries with different gold-set sizes; a raw one is a sawtooth whose shape depends on |G|.

Aggregation

every published figure

\overset{―}{M} = \frac{1}{n} \sum_{q \in Q} M_{q}, Q = {q : | G | > 0}

Macro (the mean of per-query scores), never micro (pooled hits over pooled gold): micro lets one query with 300 gold dependencies dominate a 946-query mean. Queries with no gold unit in the corpus are dropped, not scored 0. Such a query is a coverage gap, and scoring it as a miss would understate every system by the same amount — which looks like a valid comparison but is not. The count is published as n beside every row, with the dropped total behind it. Confidence intervals are a percentile bootstrap: 1000 resamples of the query set with replacement, the 2.5th and 97.5th percentiles, seeded so a rebuild cannot move a committed interval. Every metric above is a fraction in [0, 1] — the leaderboard prints three decimals, Compare prints percentages of the same number.

Which metric is shown where, and why P@k is suppressed

Every system × task emits a full curve over k = 1…200, derived from the stored per-query gold rank positions. Those positions are the source of truth: adding a metric or a finer k grid is a re-derive, never a re-retrieval, which is also why the curves can be committed as static JSON.

nDCG@k is the second curve, and on theorem search the informative one. R@k answers whether the gold declaration is inside the top k; nDCG@k answers where inside it, discounting each hit by 1⁄log₂(rank + 1). Two systems that both place the answer somewhere in the top ten have the same R@10 and can differ by a factor of three on nDCG@10, which is the difference between a reader seeing the answer and a reader scrolling for it. Relevance is binary here, and IDCG@k is normalised over min(k, gold units) — the ideal ranking has only as many relevant documents as exist, so its gain stops accruing there. Without that truncation a single-gold query’s curve would decay toward zero as k grew, which looks like a result and is an artifact. With one gold per query the definition reduces exactly to the vendored 1⁄log₂(pos + 1), and the harness tests assert that reduction so our figures stay citable against the published table.

P@k is only shown where it means something. On theorem search there is exactly one relevant declaration per query, so P@k is identically R@k⁄k — a mechanical 1⁄k decay that contains no information the recall curve does not already carry. Plotting it would imply a finding where there is only arithmetic, so the control on Compare is disabled with that explanation rather than hidden. It turns on for the multi-relevant tasks (premise selection, statement → dependencies), where gold-set sizes vary and precision is genuinely informative.

Caveats that limit comparison

Development slices are not results
A run whose corpus is a subsample carries a banner sitewide. Most gold declarations are simply absent from a slice, so its scores are computed over whichever queries survive and must not be read as a leaderboard.
Third-party engines are throttled, and may be sampled
No public engine here caps how many queries it will answer — what limits us is the courtesy rate we hold ourselves to against someone else’s free service (leansearch.net at 3 requests/30 s, LeanExplore at 24 POST/60 s against its published 30). Every response is cached permanently, so a query is only ever fetched once and that cost is paid once. This run spent it on the whole benchmark: LeanSearch v2 and LeanExplore were scored on all 894 gold-resolved queries, the same set as our own rows — so there is no n=N sampled badge and no engine_subset slice to switch to. The machinery stays for a future engine whose throttle makes the full set too expensive; until then a dashed curve on the home page marks a published engine, not a subsample.
leansearch.net’s hosted API is not the paper’s configuration
The hosted API serves a Qwen3-Reranker-4B; the paper’s Table 1 used the 8B reranker. Paper numbers are never presented as the hosted API’s.
Cross-corpus rows use the shared subset
Engines that index their own Mathlib snapshot are compared only on MathlibQR_shared171 — the 171 declarations present in every corpus involved — with a coverage column and a “different corpus” badge.
MathlibMPR is n = 69
Bootstrap 95% intervals are shown on every recall figure. At that sample size many differences are not significant, and the overlapping intervals are meant to be visible rather than hidden behind a point estimate.
LeanDojo B4 is a different corpus
It is a 2024 snapshot on older Mathlib. Its numbers are comparable to published ReProver results and not to the mathlib-4280 tasks; they are never combined into one aggregate.
NV-Embed-v2 is CC-BY-NC-4.0
Its model card states it should not be used for any commercial purpose. It is evaluated here as non-commercial research, with a license badge on its rows and a standing notice in the footer.

Prior work

These papers define the benchmarks and the protocols adopted here, and are the baseline numbers cited against.

LeanSearch v2arXiv:2605.13137
Qwen3-Embedding-8B + Qwen3-Reranker-8B. Releases MathlibQR and MathlibMPR, the two evaluation sets used here.
LeanSearch v1arXiv:2403.13310
A Semantic Search Engine for Mathlib4 — the original informalization-based approach.
LeanExplorearXiv:2506.11085
Hybrid BM25 + FAISS + reciprocal rank fusion with a dependency boost and a reranker.
Lean FinderarXiv:2510.15940
Intent-aware semantic search over Mathlib.
LeanDojo / ReProverarXiv:2306.15626
Defines the canonical tactic-state premise-selection benchmark and the R@k / MRR protocol.
Lean Hammer premise selectionarXiv:2506.07477
leanpremise.net.
Lean State SearcharXiv:2501.13959
Proof-state → premise retrieval; premise-search.com.
Textual + structural premise selectionarXiv:2510.23637
Graph-augmented premise selection on LeanDojo.
MagnushammerarXiv:2303.04488
Transformer premise selection in Isabelle — prior art for the protocol.
REAL-ProverarXiv:2505.20613
LeanSearch-PS retrieval-augmented prover.