Test "perf/magma-string-n4"
Expected: 👍 accept · Size: 16.4 MB · Lines: 342.4 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 1.2 m · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 4 with the operation table encoded as a String
satisfies x ◇ x = y ◇ ((x ◇ (y ◇ z)) ◇ z) but not
x ◇ x = x ◇ (((y ◇ x) ◇ y) ◇ z). The smallest magma of the family (4^3
tuples); the cost is dominated by decoding each table entry out of the
string on every lookup.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). The small end of the string-table
family; magma-string-pair-n9 is the same workload at a larger scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 362 ms | (÷9.6) | 235.8 MB | (×2.0) | |
| sokonanoda | 👍 | 389 ms | (÷9.0) | 335.9 MB | (×2.9) | |
| nanoclo | 👍 | 1.1 s | (÷3.2) | 211.7 MB | (+81%) | |
| con-ron | 👍 | 2.1 s | (-40%) | 283.9 MB | (×2.4) | |
| lazylean | 👍 | 1.9 s | (-46%) | 53.2 MB | (÷2.2) | |
| nanoda | 👍 | 2.0 s | (-41%) | 68.4 MB | (-42%) | |
| nanobruijn | 👍 | 2.1 s | (-40%) | 79.9 MB | (-32%) | |
| con-leche | 👍 | 5.0 s | (+43%) | 154.3 MB | (+32%) | |
| eink0rn | 👍 | 2.3 s | (-34%) | 392.7 MB | (×3.4) | |
| ind-models | 👍 | 4.4 s | (+27%) | 153.5 MB | (+31%) | |
| official | 👍 | 3.5 s | (0%) | 117.1 MB | (0%) | |
| lean4lean | 👍 | 5.1 s | (+47%) | 142.3 MB | (+22%) | |
| tenet | 👍 | 6.5 s | (+87%) | 561.9 MB | (×4.8) | |
| nanoclo-fortran | 👍 | 2.3 s | (-33%) | 189.2 MB | (+62%) | |
| lean4cobol | 👍 | 47.8 s | (×14) | 86.0 MB | (-27%) | |
| evmlean | 🚫 | 305 ms | 105.7 MB | |||
| mini | 🚫 | 39 ms | 73.4 MB | |||
| overfull | 💥 | 1.6 m | 49.0 MB | |||
| kiota | 👍 | 38.8 s | (×11) | 279.1 MB | (×2.4) | |
| canonical-min | 🚫 | 1.4 s | 1.1 GB | |||
| rpylean | 👍 | 7.4 s | (×2.1) | 1.4 GB | (×12) | |
| vow-lean-kernel | 💥 | 57.2 s | 308.8 MB | |||
| official-v4.28.0 | 👍 | 5.5 s | (+57%) | 143.2 MB | (+22%) | |
| still-nanoda | 👍 | 3.1 s | (-12%) | 75.1 MB | (-36%) | |
| nyaya | ✋ | 1.5 s | 176.0 MB | |||
| parse-only | 👍 | 923 ms | (÷3.8) | 95.6 MB | (-18%) |