Traces
Every run: the agent's full trajectory, its submissions over the 20-hour budget, and the final score.
Lean 4 Kernel Type Checker in Pascal
task page →5 runs · indexed 2026-09-02| # | Model | Reward | Cost | In tok | Out tok | Time | Steps | Submits |
|---|
| 1 | Inkling | 0.0000 | $5.56 | 5.7M | 37k | 1h 16m | 115 | 2 |
| 2 | Inkling | 0.0000 | $5.46 | 5.6M | 34k | 55m | 107 | 2 |
| 3 | Inkling | 0.0000 | $5.70 | 5.9M | 22k | 14m | 80 | 2 |
| 4 | Inkling | 0.0000 | $13.81 | 14.4M | 43k | 1h 26m | 175 | 1 |
| 5 | Inkling | 0.0000 | $6.56 | 6.8M | 25k | 12m | 109 | 6 |