Legendre
Named after Legendre, the mathematician who invented the transformation at the heart of theoretical physicsH=pq˙−L

Legendre Leaderboard: which Lean search engine is the best?

Published Lean search engines each evaluate on their own corpus with their own metrics, so their numbers are not comparable to one another — and nobody has measured how general-purpose embedding models do on Lean-specific retrieval. Every system here is scored on one pinned corpus, with one document renderer, using exact search with no approximate index to confound the result. Every system publishes a full R@k curve, not a cut-off.

Recall curves

A cut-off is a single point on a curve, and two systems with the same nDCG@10 can climb very differently. Everything here is derived from the stored per-query rank positions and shipped as static JSON, so the curves render with no backend and no runtime compute.

Task
Systems
Max lines
MetricP@k suppressed — single relevant declaration per query; nDCG@k is the rank-sensitive one that still applies
Breakdown
Recall@k — Theorem search
MathlibQR — the theorem-search benchmark released with the LeanSearch v2 paper, used here unmodified — pairs 200 Mathlib declarations with up to 6 differently worded queries each — one per style (Lean-ish, LaTeX, Natural language, Slogan, Nickname, Special case) — 946 in all, because 254 of the 1,200 slots are blank in the source: not every theorem has a nickname or a memorable special case. Exactly one declaration is relevant per query, so R@k asks only whether the right one landed in the top k — precision would be a mechanical R@k/k decay and is suppressed, while nDCG@k asks the sharper question of where in the top k it landed. Gold is resolved by full_name against mathlib-4280 (310,579 declarations); 11 of the 200 are absent at the pinned revision, so their queries are reported unresolved rather than counted as misses. Dashed curves are published Lean search engines we did not run ourselves: we queried each one over its public HTTP API — LeanSearch v2 at POST leansearch.net/search and LeanExplore at POST leanexplore.com/api/v2/search — sending it every benchmark query and scoring the ranking it returned. So the embedding model, the index and the reranker behind those curves are theirs, running on their hardware against their own corpus snapshot, and only the queries and the metrics are ours. They share a hue with one of our systems, so the stroke is what tells them apart. LeanSearch v2 ends at k=50 — that service returns no more results, so the metric above it is undefined rather than flat.
k=10k=20k=50k=1001251020501002000%20%40%60%80%100%k (log scale)Recall@kNemotron3-8BQwen3-4BQwen3-8BLeanSearch v2LeanExploreNemotron3-1BQwen3-0.6BEmbGemma-300MBM25BGE-M3
  • LeanSearch v2published
  • Nemotron3-8B
  • Qwen3-8B
  • Qwen3-4B
  • LeanExplorepublished
  • Nemotron3-1B
  • Qwen3-0.6B
  • BGE-M3
  • EmbGemma-300M
  • BM25

At k = 10

Best embedding model
0.526
Nemotron-3-Embed-8B
Lead over next
+15.4%
vs Qwen3-Embedding-8B — check the bootstrap interval on R@10 before calling it significant
Best published engine
0.571
LeanSearch v2 — on the same 894 queries, so this one is directly comparable to the tile on the left
Queries scored
894
of 946 in MathlibQR; the remainder have a gold declaration absent from this corpus

The leaderboard has the same systems as a sortable table with model metadata, licenses and latency; explore the datasets to see the ground-truth pairs behind every number, or run a live query against these systems side by side.