Theorem Proving on CLEVER (examples)
5Solved Tests (Correct Entries)Numina Lean Agent
Evaluation results
| Method | Links | ||
|---|---|---|---|
| Numina Lean AgentBenchmark variant=P2026.05 | 5 | 1 | |
| Claude Code + lean4-skillsBenchmark variant=P2026.05 | 5 | 1 | |
| AristotleBenchmark variant=PM2026.05 | 5 | — | |
| Kimina-ProverBenchmark variant=P2026.05 | 4 | — | |
| GrindBenchmark variant=PU2026.05 | 2 | — | |
| LeanHammerBenchmark variant=PU2026.05 | 1 | — | |
| AesopBenchmark variant=PU2026.05 | 1 | — | |
| CanonicalBenchmark variant=PU2026.05 | 0 | — |