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.4 s | (÷20) | 2.0 GB | (-17%) | |
| mathgraph | 👍 | 44.9 s | (÷15) | 1.9 GB | (-25%) | |
| nanoclo | 👍 | 3.1 m | (÷3.6) | 2.6 GB | (+6%) | |
| con-ron | 👍 | 3.3 m | (÷3.4) | 1.7 GB | (-32%) | |
| nanobruijn | 👍 | 6.2 m | (-45%) | 1.7 GB | (-30%) | |
| nanoda | 👍 | 8.2 m | (-27%) | 1.6 GB | (-36%) | |
| lazylean | 👍 | 6.6 m | (-41%) | 1.8 GB | (-29%) | |
| con-leche | 👍 | 7.6 m | (-32%) | 1.4 GB | (-43%) | |
| tenet-jvm | 👍 | 8.2 m | (-27%) | 5.7 GB | (×2.3) | |
| eink0rn | 👍 | 11.5 m | (+3%) | 4.3 GB | (+74%) | |
| official | 👍 | 11.2 m | (0%) | 2.5 GB | (0%) | |
| ind-models | 👍 | 13.3 m | (+18%) | 1.6 GB | (-36%) | |
| lean4lean | 👍 | 13.3 m | (+18%) | 2.9 GB | (+17%) | |
| tenet | 👍 | 18.6 m | (+66%) | 6.2 GB | (×2.5) | |
| tenet-hs | 👍 | 18.2 m | (+62%) | 3.0 GB | (+23%) | |
| lean4cobol | 🚫 | 20.3 m | 1.7 GB | |||
| evmlean | 🚫 | 307 ms | 106.3 MB | |||
| mini | 🚫 | 39 ms | 73.9 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | 🚫 | 58.7 s | 599.2 MB | |||
| 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%) |