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

Lean type to informal description retrieval on mathlib (test)

72.77R@1MathLeap-Octen-8B

Evaluation Results

Method	Links
MathLeap-Octen-8B2026.06		72.77	92.33	94.77	81.37
MathLeap-Qwen-8B2026.06		71.28	91.98	94.45	80.33
MathLeap-Octen-8B2026.06		66.89	86.54	89.92	75.57
MathLeap-Qwen-8B2026.06		65.22	85.77	89.29	74.26
Octen-Embedding-8B2026.06		58.17	85.56	90.07	69.9
F2LLM-v2-14B2026.06		57.51	84.36	89.47	69.1
Octen-Embedding-8B2026.06		57.44	82.94	87.94	68.48
F2LLM-v2-14B2026.06		56.78	85.02	90.09	68.93
Qwen3-Embedding-4B2026.06		47.1	73.93	80.39	58.65
Qwen3-Embedding-4B2026.06		45.33	75	82.4	57.98
Qwen3-Embedding-8B2026.06		44.97	74.9	82.61	57.69
KaLM-Gemma3-12B2026.06		43.36	70.78	78.09	55.12
Qwen3-Embedding-8B2026.06		42.39	70.67	78.16	54.5
KaLM-Gemma3-12B2026.06		42.31	71.3	79.43	54.69
Harrier-OSS-v1-27B2026.06		38.47	66.16	74.51	50.29
Harrier-OSS-v1-27B2026.06		33.03	61.87	71.53	45.33
Llama-Embed-Nemotron-8B2026.06		2.62	6.73	9.66	4.43
Llama-Embed-Nemotron-8B2026.06		1.17	3.56	5.78	2.3