Test "perf/magma-list-deep-n21"
Expected: 👍 accept · Size: 1.1 MB · Lines: 21.6 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 1.3 m · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 21 with an inline List operation table satisfies
x = (x ◇ x) ◇ (x ◇ (y ◇ y)) but not x = x ◇ (x ◇ x). The search space is
only 21^2 tuples, but each equation nests the operation several deep, so
every tuple expands into a chain of linear list lookups.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). The small end of the deep-nesting
family; magma-list-deep-n36 is the same workload at a larger scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 349 ms | (÷6.5) | 674.2 MB | (+21%) | |
| sokonanoda | 👍 | 361 ms | (÷6.2) | 674.1 MB | (+21%) | |
| nanoclo | 👍 | 176 ms | (÷13) | 148.3 MB | (÷3.8) | |
| con-ron | 👍 | 1.7 s | (-24%) | 450.8 MB | (-19%) | |
| lazylean | 👍 | 389 ms | (÷5.8) | 29.3 MB | (÷19) | |
| nanoda | 👍 | 1.9 s | (-17%) | 216.0 MB | (÷2.6) | |
| nanobruijn | 👍 | 1.6 s | (-30%) | 209.7 MB | (÷2.7) | |
| con-leche | 👍 | 3.4 s | (+51%) | 598.7 MB | (+7%) | |
| eink0rn | 👍 | 1.4 s | (-39%) | 615.9 MB | (+10%) | |
| ind-models | 👍 | 2.4 s | (+6%) | 589.9 MB | (+6%) | |
| official | 👍 | 2.3 s | (0%) | 557.8 MB | (0%) | |
| lean4lean | 👍 | 3.0 s | (+31%) | 585.1 MB | (+5%) | |
| tenet | 👍 | 2.6 s | (+15%) | 1.2 GB | (×2.2) | |
| nanoclo-fortran | 👍 | 896 ms | (÷2.5) | 452.8 MB | (-19%) | |
| lean4cobol | 👍 | 37.9 s | (×17) | 364.1 MB | (-35%) | |
| evmlean | 🚫 | 306 ms | 106.3 MB | |||
| mini | 🚫 | 83 ms | 75.1 MB | |||
| overfull | 💥 | 1.6 m | 49.2 MB | |||
| kiota | 👍 | 1.8 s | (-21%) | 307.7 MB | (-45%) | |
| canonical-min | 🚫 | 455 ms | 1.1 GB | |||
| rpylean | 👍 | 6.1 s | (×2.7) | 1.4 GB | (×2.5) | |
| vow-lean-kernel | 💥 | 47.8 s | 314.0 MB | |||
| official-v4.28.0 | 👍 | 7.6 s | (×3.4) | 959.1 MB | (+72%) | |
| still-nanoda | 👍 | 1.7 s | (-23%) | 216.1 MB | (÷2.6) | |
| nyaya | ✋ | 333 ms | 47.6 MB | |||
| parse-only | 👍 | 89 ms | (÷25) | 69.6 MB | (÷8.0) |