Theorem Proving on CLEVER human_eval
27Solved Tests (Correct)Numina Lean Agent
Evaluation results
| Method | Links | ||
|---|---|---|---|
| Numina Lean AgentBenchmark variant=P2026.05 | 27 | 14 | |
| Claude Code + lean4-skillsBenchmark variant=P2026.05 | 26 | 8 | |
| AristotleBenchmark variant=PM2026.05 | 23 | 9 | |
| Kimina-ProverBenchmark variant=P2026.05 | 3 | — | |
| GrindBenchmark variant=PU2026.05 | 3 | 1 | |
| LeanHammerBenchmark variant=PU2026.05 | 3 | — | |
| AesopBenchmark variant=PU2026.05 | 2 | — | |
| CanonicalBenchmark variant=PU2026.05 | 0 | — |