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

Changelog

What each release added and what it did to the ranking. Every figure below is the figure that was published on that date, so an entry never changes once it is written — each one names the commit that wrote its artifact, which is what makes it checkable rather than merely stated.

  1. Lean Finder v2 added — first, by a margin the intervals support

    Added Lean Finder v2 over the authors’ public endpoint, taking the board to 14 systems — all 894 gold-resolved queries, curves to k=200. It is built on lean-finder-v2-base, a Qwen3-Embedding-8B fine-tune with no paper yet and unpublished training data, so overlap with MathlibQR’s queries cannot be checked. We query it at v4.28.0, whose rebuilt index now has structures and classes; every name it returned exists in our corpus. v1’s endpoint now serves v2, so the v1 row stands on our archived September responses and leaves the playground.

    First at nDCG@10 0.7254, R@1 55.0%, R@10 89.4%, R@100 97.3% — and unlike the last two releases, the lead is not a tie: +0.134 nDCG@10 over Lean Finder v1, 95% [+0.108, +0.161], and +0.154 over LeanSearch v2, 95% [+0.128, +0.180]. Against its own base, Qwen3-Embedding-8B, the gain is +0.269. Its weakest style is q4_special_case (nDCG@10 0.19, n=23); its strongest is natural language (0.797).

    run m1 · commit ef0fc2d · git show ef0fc2d:web/data/results/m1/leaderboard.json

  2. Lean Finder v1 added — first on the board, by a margin that is not one

    Added Lean Finder v1 over the authors’ JSON inference endpoint, taking the board to 13 systems — all 894 gold-resolved queries, no subsample, curves to k=200. It is the only hosted engine that lets a caller pick the Mathlib snapshot, and we ask it for v4.19.0 rather than the one matching this corpus: its newer indexes contain no structures or classes, which a third of these queries need. That is a nine-release version delta, so more of what it returns is absent from our corpus and scored as a miss; Methodology has the measurement.

    First as the board sorts: nDCG@10 0.5913, R@1 45.7%, R@10 72.6%, R@200 90.3%. Not a win, though — the nDCG@10 margin over MathLeap-Qwen-8B is +0.019, 95% [−0.007, +0.046], p≈0.16, and R@10 is a three-way tie with MathLeap’s 72.8% and LeanSearch v2’s 74.4%. What is separated is the first slot: R@1 +5.5 pt over LeanSearch v2, 95% [+1.9, +9.2], p≈0.003. Its best query style is q3_nickname (nDCG@10 0.6718) and its weakest is Lean syntax (0.5364) — the opposite profile to a lexical retriever.

    run m1 · commit 1a20e42 · git show 1a20e42:web/data/results/m1/leaderboard.json

  3. MathLeap fine-tunes added — a fine-tune reaches the top

    Added the two MathLeap 8B checkpoints — MathLeap-Qwen-8B and MathLeap-Octen-8B — taking the board from 10 systems to 12. Both were scored on the same 894 gold-resolved MathlibQR queries, the same corpus revision and the same document renderer as every existing row, so their curves went up beside the others without re-running anything else.

    MathLeap-Qwen-8B takes the top of the board as it sorts by default: nDCG@10 0.5722 against LeanSearch v2’s 0.5712, with MRR 0.529 vs 0.519, R@1 42.4% vs 40.3% and R@50 83.8% vs 78.9%. Two things that ranking does not support: the nDCG@10 margin is 0.001, and R@10 still goes to LeanSearch v2 — 74.4% against 72.8%, with bootstrap intervals [71.6, 77.3] and [69.8, 76.0] that overlap across most of their width, so that column is a tie and not a pass. The separation that is real is at k ≥ 20, where MathLeap keeps climbing and the hosted LeanSearch v2 API stops returning results at k=50.

    run m1 · commit 164bece · git show 164bece:web/data/results/m1/leaderboard.json

  4. First published run — the Lean-specific engine beats every embedding model

    The board went live: 10 systems on MathlibQR over the full mathlib-4280 corpus — 310,579 declarations — with R@k and nDCG@k curves to k=200 rather than a handful of cut-offs. Eight systems of ours (BM25, Qwen3-Embedding 0.6B/4B/8B, Nemotron-3-Embed 1B/8B, EmbeddingGemma-300M, BGE-M3) and two published engines queried over their own public HTTP APIs, every row on all 894 gold-resolved queries with no subsample.

    LeanSearch v2 led, at nDCG@10 0.5712 and R@10 74.4%, ahead of the best general-purpose embedding model — Nemotron-3-Embed-8B at 0.5261 and 68.3%. A Lean-specific engine with a reranker beating every off-the-shelf embedding model, by roughly 6 points of recall, was the run’s finding.

    run m1 · commit 61d54c2 · git show 61d54c2:web/data/results/m1/leaderboard.json

Every entry above shares run m1: the corpus revision, the document renderer and the metric code never changed between them, so a row added in any release is directly comparable to every other. A release that changes any of those gets a new run id, and this page will say so — comparing across it would not be sound.

Want your model, engine or benchmark here? Scoring one more row costs a matmul against vectors that already exist, so the answer is usually yes — send the link and the license and it goes in the next release.