Legendreleaderboard for Mathlib search engines and embeddings

Named after Legendre, the mathematician who invented the transformation at the heart of theoretical physics

H = p \dot{q} - L

(H = p\dot{q} - L)

Playground

One query, up to three systems, side by side against 310,579 declarations of mathlib-4280. Columns stream independently, so a lexical result appears immediately while a larger model is still warming up — and a backend that fails takes only its own column down.