Test "mathlib"
Expected: 👍 accept · Size: 5.2 GB · Lines: 100.0 M · lean4export: 3.1.0 · Lean: 4.29.0 · 📄 Declaration · 🔗 Source
The complete Mathlib library export.
This test contains all the mathematical definitions, theorems, and proofs from Mathlib, representing the largest and most comprehensive test case in the Lean kernel arena.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| nanoda | 👍 | 23.4 m | (-28%) | 7.9 GB | (-13%) | |
| nanobruijn | 👍 | 27.7 m | (-16%) | 5.5 GB | (-39%) | |
| official-nightly | 👍 | 31.9 m | (-3%) | 9.2 GB | (0%) | |
| official | 👍 | 32.8 m | (0%) | 9.1 GB | (0%) | |
| official-v4.28.0 | 👍 | 42.0 m | (+28%) | 9.3 GB | (+2%) | |
| mini | 🚫 | 42 ms | 70.3 MB | |||
| evmlean | 🚫 | 361 ms | 88.0 MB | |||
| always-decline | 🚫 | 1 ms | 2.8 MB | |||
| lean4lean | ✋ | 16.8 m | 8.7 GB | |||
| still-nanoda | 👍 | 16.1 m | (-51%) | 5.2 GB | (-43%) | |
| rpylean | ✋ | 17.6 m | 14.2 GB | |||
| always-reject | ✋ | 1 ms | 2.8 MB | |||
| sokonanoda | 👍 | 9.7 m | (-70%) | 7.3 GB | (-20%) | |
| parse-only | 👍 | 5.3 m | (-84%) | 8.6 GB | (-6%) | |
| always-accept | 👍 | 1 ms | (-100%) | 2.8 MB | (-100%) |