Theorem Retrieval on Raw Proof State
8.3Recall@1Lean Finder
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| Lean Finder2025.10 | 8.3 | 30.1 | 40 | 0.19 | |
| Real Prover Search2025.10 | 7.1 | 26.2 | 34.3 | 0.16 | |
| GPT-4oMatching strategy=stem match2025.10 | 6.4 | 11.5 | 13.6 | — | |
| GPT-4oMatching strategy=full name match2025.10 | 4.5 | 8.5 | 9.9 | — | |
| Lean State Search2025.10 | 3.3 | 23.1 | 32.1 | 0.13 |