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, Lean Finder at 1/s against a published 100 per minute). 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 and Lean Finder v1 and Lean Finder v2 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.
The MathLeap rows are in-domain, not zero-shot
Every other model here saw no Lean during training, so its score measures transfer. The two MathLeap checkpoints were fine-tuned for exactly this task, on Mathlib statements paired with their informalizations from FrenzyMath/mathlib_informal_v4.16.0 — the same declarations and the same informalization family that mathlib-4280 renders, one Mathlib snapshot apart. That a task-specific fine-tune wins a task is the finding, not a problem; reading its number as a zero-shot result would be the error, so their rows carry an in-domain badge and the caption under the curves names them. MathLeap-Qwen-8B shares its base model, its dimensionality, its pooling and its prompt format with Qwen3-Embedding-8B, so plot both and the gap between those two curves is the fine-tune with everything else held fixed — the one controlled comparison this board contains, and the caption on the home page says so whenever both are selected.
We override MathLeap’s sequence length from 128 to 32768
Both repos ship max_seq_length: 128 and we do not honor it: that is a Sentence-Transformers setting saved from their training run, while config.json declares 40960 positions in both. It matters because 51.6% of this corpus’s rendered documents exceed 128 tokens and the renderer puts informal text first, so the cut lands almost exactly where the Lean declaration begins — honoring it would index half the corpus with the formal content removed. So the harness pins max_ctx = 32768, declares the shipped 128 beside it, and raises the limit at load time: our override, not a claim these checkpoints make. Its cost is that positions past 128 were seen by the base model but never during the fine-tune.
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.
MathLeaparXiv:2606.23959
Does My Embedding Reflect That A=B? — multi-view contrastive fine-tuning of Qwen3-Embedding-8B and Octen-Embedding-8B on Mathlib statements and their informalizations. The two MathLeap rows here are its released checkpoints.
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; the paper describes v1. v1 was scored in September at the v4.19.0 snapshot, because the endpoint's newer indexes then held no structures or classes. That endpoint now serves v2, so the v1 row is scored from our archived responses and is not offered in the playground. v2 has no paper yet: it is built on lean-finder-v2-base, a Qwen3-Embedding-8B fine-tune, and is queried at v4.28.0, whose index now includes structures and classes.
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.