Test "reachability"
Expected: 👍 accept · Size: 18.1 MB · Lines: 361.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 15.2 min · 📄 Declaration · 🔗 Source
Reachability: verified, kernel-reducible
reachability and shortest walks for finite directed graphs, built on Mathlib.
Its breadth-first search is plain structural recursion, so the examples are proved with
decide +kernel, which makes the kernel evaluate the search itself. This test exports
named proofs for paths, grids, sparse random graphs, a dense DAG, and a shortest walk,
together with only their dependencies.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 2.95 s | (÷8.0) | 3.6 GB | (×2.2) | |
| nano-lean | 👍 | 1.93 s | (÷12) | 1.3 GB | (-21%) | |
| sokonanoda | 👍 | 4.00 s | (÷5.9) | 1.5 GB | (-9%) | |
| pestka | 👍 | 3.89 s | (÷6.0) | 337.9 MB | (÷5.0) | |
| kefir | 👍 | 3.28 s | (÷7.2) | 354.2 MB | (÷4.7) | |
| nanoclo | 👍 | 3.49 s | (÷6.7) | 1.6 GB | (0%) | |
| kefir-wasm | 👍 | 5.40 s | (÷4.4) | 636.2 MB | (÷2.6) | |
| con-ron | 👍 | 15.6 s | (-34%) | 2.5 GB | (+51%) | |
| con-agua | 👍 | 23.3 s | (-1%) | 2.5 GB | (+53%) | |
| nanoda | 👍 | 21.0 s | (-11%) | 2.1 GB | (+26%) | |
| lazylean | 👍 | 3.24 s | (÷7.3) | 192.8 MB | (÷8.7) | |
| con-leche | 👍 | 31.6 s | (+34%) | 4.4 GB | (×2.7) | |
| pestka-wasm | 👍 | 12.3 s | (-48%) | 1.2 GB | (-24%) | |
| tenet-jvm | 👍 | 20.9 s | (-11%) | 4.3 GB | (×2.6) | |
| eink0rn | 👍 | 22.4 s | (-5%) | 4.0 GB | (×2.5) | |
| official | 👍 | 23.5 s | (0%) | 1.6 GB | (0%) | |
| ind-models | 👍 | 24.7 s | (+5%) | 1.6 GB | (0%) | |
| lean4lean | 👍 | 32.1 s | (+36%) | 1.7 GB | (+2%) | |
| tenet | 👍 | 46.1 s | (+96%) | 6.5 GB | (×4.0) | |
| tenet-hs | 👍 | 43.7 s | (+86%) | 1.1 GB | (-35%) | |
| ocaml4lean | 👍 | 40.1 s | (+71%) | 6.2 GB | (×3.8) | |
| lean4cobol | 👍 | 6.68 min | (×17) | 2.1 GB | (+27%) | |
| evmlean | 🚫 | 306 ms | 106.3 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 318 ms | 81.9 MB | |||
| canonical-min | ✋ | 1.48 s | 1.1 GB | |||
| kiota | 👍 | 23.6 s | (0%) | 2.0 GB | (+24%) | |
| metalean-slow | 🚫 | 1.08 s | 83.9 MB | |||
| nanobruijn | 👍 | 16.0 s | (-32%) | 1.9 GB | (+15%) | |
| metalean-fast | 👍 | 37.3 s | (+59%) | 4.5 GB | (×2.8) | |
| nanoclo-fortran | 👍 | 13.3 s | (-43%) | 5.9 GB | (×3.6) | |
| rpylean | ⌛ | 0 ms | 0 B | |||
| mathgraph | 👍 | 7.27 s | (÷3.2) | 5.7 GB | (×3.5) | |
| parse-only | 👍 | 1.01 s | (÷23) | 99.3 MB | (÷17) |