Test "perf/magma-string-n4"
Expected: 👍 accept · Size: 16.5 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 70.0 s · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 200 ms | (÷18) | 221.2 MB | (+82%) | |
| nano-lean | 👍 | 233 ms | (÷15) | 376.8 MB | (×3.1) | |
| sokonanoda | 👍 | 267 ms | (÷13) | 290.3 MB | (×2.4) | |
| pestka | 👍 | 548 ms | (÷6.5) | 133.3 MB | (+10%) | |
| kefir | 👍 | 795 ms | (÷4.5) | 82.3 MB | (-32%) | |
| nanoclo | 👍 | 1.10 s | (÷3.2) | 215.8 MB | (+78%) | |
| kefir-wasm | 👍 | 1.83 s | (-48%) | 211.1 MB | (+74%) | |
| con-ron | 👍 | 2.05 s | (-42%) | 224.3 MB | (+85%) | |
| con-agua | 👍 | 3.11 s | (-12%) | 126.5 MB | (+4%) | |
| nanoda | 👍 | 2.09 s | (-41%) | 63.3 MB | (-48%) | |
| lazylean | 👍 | 1.84 s | (-48%) | 55.1 MB | (÷2.2) | |
| con-leche | 👍 | 4.92 s | (+39%) | 137.9 MB | (+14%) | |
| pestka-wasm | 👍 | 2.84 s | (-20%) | 732.6 MB | (×6.0) | |
| tenet-jvm | 👍 | 4.88 s | (+38%) | 745.8 MB | (×6.1) | |
| eink0rn | 👍 | 2.38 s | (-33%) | 401.0 MB | (×3.3) | |
| official | 👍 | 3.55 s | (0%) | 121.3 MB | (0%) | |
| ind-models | 👍 | 4.16 s | (+17%) | 166.6 MB | (+37%) | |
| lean4lean | 👍 | 5.25 s | (+48%) | 146.8 MB | (+21%) | |
| tenet | 👍 | 6.56 s | (+85%) | 669.5 MB | (×5.5) | |
| tenet-hs | 👍 | 3.93 s | (+11%) | 171.2 MB | (+41%) | |
| ocaml4lean | 👍 | 3.86 s | (+9%) | 177.0 MB | (+46%) | |
| lean4cobol | 👍 | 49.5 s | (×14) | 92.6 MB | (-24%) | |
| evmlean | 🚫 | 307 ms | 103.9 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 38.8 ms | 73.9 MB | |||
| canonical-min | 🚫 | 1.39 s | 1.1 GB | |||
| kiota | 👍 | 3.07 s | (-14%) | 310.1 MB | (×2.6) | |
| metalean-slow | 🚫 | 771 ms | 83.2 MB | |||
| nanobruijn | 👍 | 2.13 s | (-40%) | 80.8 MB | (-33%) | |
| metalean-fast | 👍 | 7.04 s | (+98%) | 232.9 MB | (+92%) | |
| nanoclo-fortran | 👍 | 2.37 s | (-33%) | 207.8 MB | (+71%) | |
| rpylean | 👍 | 7.37 s | (×2.1) | 1.3 GB | (×11) | |
| mathgraph | 👍 | 361 ms | (÷9.8) | 219.8 MB | (+81%) | |
| parse-only | 👍 | 926 ms | (÷3.8) | 95.5 MB | (-21%) |