Test "perf/refute-cheap-last"
Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.29.1 · 📄 Declaration · 🔗 Source
The declaration to check claims
(count #n, false) = (count #(n+1), true)
and must be rejected: refute-cheap-first.lean with the components swapped,
so the cheap refutation sits behind the expensive one for a checker that
visits components left to right.
N=200 in the Lean source. From Courant and Leroy, POPL 2026, §10.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 3 ms | 42.1 MB | |||
| ind-models | ✋ | 723 ms | 103.6 MB | |||
| official-nightly | ✋ | 176 ms | 65.5 MB | |||
| evmlean | 🚫 | 1.9 s | 135.7 MB | |||
| nanoda | ✋ | 34 ms | 3.5 MB | |||
| mini | 💥 | 1.6 m | 78.5 MB | |||
| lean4lean | ✋ | 1.3 s | 102.0 MB | |||
| sokonanoda | ✋ | 3 ms | 42.0 MB | |||
| zignodamus | ✋ | 11 ms | 12.3 MB | |||
| nanoclo | ✋ | 19 ms | 53.7 MB | |||
| nanobruijn | ✋ | 24 ms | 12.4 MB | |||
| kiota | ✋ | 4 ms | 12.9 MB | |||
| official | ✋ | 692 ms | 65.7 MB | |||
| vow-lean-kernel | ✋ | 138 ms | 11.0 MB | |||
| rpylean | ✋ | 298 ms | 41.8 MB | |||
| official-v4.28.0 | ✋ | 774 ms | 72.7 MB | |||
| still-nanoda | ✋ | 34 ms | 3.3 MB | |||
| nyaya | 💥 | 1.7 m | 16.2 MB | |||
| parse-only | 👍 | 28 ms | 60.6 MB |