Theorem Retrieval on Lean Synthetic User Query (Sec. 3.1)
54.4Recall@1Lean Finder
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| Lean Finder2025.10 | 54.4 | 84.4 | 91.4 | 0.68 | |
| Lean Search2025.10 | 47.1 | 77.7 | 83.7 | 0.6 | |
| GPT-4omatching strategy=stem match2025.10 | 17.8 | 27.4 | 30.5 | — | |
| GPT-4omatching strategy=full name match2025.10 | 13.6 | 21.5 | 23.3 | — |