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.
full_name against mathlib-4280 (310,579 declarations); 11 of the 200 are absent at the pinned revision, so their queries count as unresolved, not misses. Dashed curves are engines we did not run: every benchmark query was POSTed to the service its authors operate — Lean Finder v2 at POST lean-lsp-proxy.leanfinder.workers.dev, Lean Finder v1 at POST bxrituxuhpc70w8w.us-east-1.aws.endpoints.huggingface.cloud, LeanSearch v2 at POST leansearch.net/search and LeanExplore at POST leanexplore.com/api/v2/search — and the ranking that came back is what is scored. The model, the index, the reranker and the corpus snapshot behind those curves are theirs; only the queries and the metrics are ours. MathLeap-Qwen (from Qwen3-Embedding-8B) and MathLeap-Octen (from Octen-Embedding-8B, itself a Qwen3-Embedding-8B fine-tune) were fine-tuned for this task on Mathlib informalizations from the same source family this corpus renders, one snapshot apart, so their numbers are in-domain rather than zero-shot. MathLeap-Qwen and Qwen3-8B are the same weights before and after that training and both are plotted, holding architecture, dimensionality, pooling and prompt format fixed. LeanSearch v2 ends at k=50: the service returns no more results, so the metric is undefined above that rather than flat.- Lean Finder v2published engine
- Lean Finder v1published engine
- MathLeap-Qwen
- LeanSearch v2published engine
- MathLeap-Octen
- Nemotron3-8B
- Qwen3-8B
- Qwen3-4B
- LeanExplorepublished engine
- Nemotron3-1B
- Qwen3-0.6B
- BGE-M3
- EmbGemma-300M
- BM25
| System | n | R@1 | R@5 | R@10 | R@20 | R@50 | R@100 |
|---|---|---|---|---|---|---|---|
| Lean Finder v2 | 894 | 55.0% | 82.8% | 89.4% | 92.4% | 95.6% | 97.3% |
| Lean Finder v1 | 894 | 45.7% | 66.6% | 72.6% | 78.4% | 83.6% | 86.9% |
| MathLeap-Qwen | 894 | 42.4% | 65.3% | 72.8% | 78.3% | 83.8% | 87.8% |
| LeanSearch v2k≤50 | 894 | 40.3% | 67.7% | 74.4% | 77.9% | 78.9% | n/a |
| MathLeap-Octen | 894 | 41.4% | 64.3% | 71.6% | 77.7% | 83.1% | 86.9% |
| Nemotron3-8B | 894 | 36.9% | 62.3% | 68.3% | 74.0% | 79.5% | 83.7% |
| Qwen3-8B | 894 | 31.9% | 53.4% | 60.1% | 65.8% | 73.9% | 77.9% |
| Qwen3-4B | 894 | 29.2% | 49.8% | 57.3% | 64.0% | 72.5% | 77.7% |
| LeanExplore | 894 | 23.4% | 45.5% | 56.5% | 65.5% | 74.7% | 78.7% |
| Nemotron3-1B | 894 | 21.1% | 43.5% | 51.0% | 60.1% | 69.5% | 73.9% |
| Qwen3-0.6B | 894 | 21.1% | 38.8% | 46.4% | 52.5% | 60.9% | 66.9% |
| BGE-M3 | 894 | 16.8% | 31.2% | 37.9% | 43.4% | 50.7% | 56.3% |
| EmbGemma-300M | 894 | 14.3% | 29.0% | 36.1% | 44.1% | 51.8% | 58.3% |
| BM25 | 894 | 14.7% | 26.2% | 32.6% | 39.0% | 47.1% | 53.9% |
At k = 10
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.