Theorem Retrieval on Augmented Proof State
0.246R@1Lean Finder
Evaluation results
| Method | Links | ||||
|---|---|---|---|---|---|
| Lean Finder2025.10 | 0.246 | 0.568 | 0.679 | 0.4 | |
| GPT-4oMatching strategy=stem match2025.10 | 0.101 | 0.173 | 0.197 | — | |
| Real Prover Search2025.10 | 0.08 | 0.29 | 0.392 | 0.18 | |
| GPT-4oMatching strategy=full name match2025.10 | 0.074 | 0.133 | 0.15 | — | |
| Lean State Search2025.10 | 0.0499 | 0.277 | 0.396 | 0.16 |