Test "navier-stokes-euler"
Expected: 👍 accept · Size: 1.5 GB · Lines: 28.6 M · lean4export: 3.1.0 · Lean: 4.34.0-rc2 · Timeout: 40.0 m · 📄 Declaration · 🔗 Source
OpenAI's Lean formalization of finite-time blowup for the three-dimensional incompressible Navier–Stokes equations with smooth forcing (on Euclidean space and on the periodic torus), and of unforced Euler blowup. See https://github.com/openai/NavierStokesAndEuler/.
This test exports the main results listed in the project's formalization.yaml,
together with their dependencies.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | 👍 | 34.3 s | (÷20) | 2.1 GB | (-17%) | |
| mathgraph | 👍 | 45.1 s | (÷15) | 1.9 GB | (-24%) | |
| nanoclo | 👍 | 3.1 m | (÷3.6) | 2.6 GB | (+5%) | |
| con-ron | 👍 | 3.6 m | (÷3.1) | 1.8 GB | (-27%) | |
| nanobruijn | 👍 | 6.5 m | (-42%) | 1.7 GB | (-30%) | |
| nanoda | 👍 | 8.2 m | (-27%) | 1.6 GB | (-36%) | |
| lazylean | 👍 | 6.6 m | (-41%) | 1.8 GB | (-29%) | |
| con-leche | 👍 | 9.1 m | (-19%) | 1.7 GB | (-31%) | |
| eink0rn | 👍 | 11.5 m | (+3%) | 4.2 GB | (+71%) | |
| official | 👍 | 11.2 m | (0%) | 2.5 GB | (0%) | |
| ind-models | 👍 | 13.3 m | (+18%) | 1.6 GB | (-36%) | |
| lean4lean | 👍 | 13.3 m | (+19%) | 2.9 GB | (+17%) | |
| tenet | 👍 | 18.6 m | (+65%) | 6.4 GB | (×2.6) | |
| tenet-hs | 👍 | 18.2 m | (+62%) | 3.0 GB | (+22%) | |
| lean4cobol | 🚫 | 20.3 m | 1.7 GB | |||
| evmlean | 🚫 | 308 ms | 106.8 MB | |||
| mini | 🚫 | 39 ms | 74.5 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 58.7 s | 599.4 MB | |||
| tenet-jvm | ✋ | 2.6 m | 5.6 GB | |||
| nanoclo-fortran | 👍 | 11.0 m | (-2%) | 5.0 GB | (×2.0) | |
| kiota | ⌛ | 0 ms | 0 B | |||
| metalean-fast | 👍 | 29.4 m | (×2.6) | 5.8 GB | (×2.3) | |
| canonical-min | 🚫 | 1.4 m | 3.8 GB | |||
| rpylean | 🚫 | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| parse-only | 👍 | 1.3 m | (÷8.7) | 2.5 GB | (0%) |