Formal Mathematics Retrieval on User Study Real-world Queries
139R@1Lean Finder
Evaluation Results
| Method | Links | |||||
|---|---|---|---|---|---|---|
| Lean Finder2025.10 | 139 | 56 | 36 | 81.6 | 0.67 | |
| GPT-4o2025.10 | 71 | 46 | 36 | 54.1 | 0.4 | |
| Lean Search2025.10 | 70 | 51 | 40 | 56.9 | 0.41 |
Loading the SOTA2 catalog…
| Method | Links | |||||
|---|---|---|---|---|---|---|
| Lean Finder2025.10 | 139 | 56 | 36 | 81.6 | 0.67 | |
| GPT-4o2025.10 | 71 | 46 | 36 | 54.1 | 0.4 | |
| Lean Search2025.10 | 70 | 51 | 40 | 56.9 | 0.41 |