Informal description to Lean type retrieval on mathlib (test) benchmark leaderboard · SOTA2 Research

Informal description to Lean type retrieval on mathlib (test)

70.18R@1MathLeap-Octen-8B

Evaluation Results

Method	Links
MathLeap-Octen-8B2026.06		70.18	88.27	91.64	78.26
MathLeap-Qwen-8B2026.06		69.34	88.35	91.72	77.77
F2LLM-v2-14B2026.06		67.97	90.42	93.36	77.78
Octen-Embedding-8B2026.06		64.06	87.91	91.43	74.47
Harrier-OSS-v1-27B2026.06		62.26	87.9	91.67	73.37
Qwen3-Embedding-8B2026.06		61.89	86.7	90.71	72.65
Qwen3-Embedding-4B2026.06		57.01	84.33	89.08	68.79
KaLM-Gemma3-12B2026.06		56.32	82.25	87.49	67.54
Llama-Embed-Nemotron-8B2026.06		27.87	52.79	61.72	38.42