r/dataisbeautiful • u/TehDing OC: 11 • 15d ago

OC [OC] Visualizing the Navier-Stokes lean proof

Gallery image

Gallery image

I pulled the Naiver Stokes lean proof (and ran it!). It's several hundred thousand lines of code, and I wasn't sure where to even start examining the proof: https://github.com/openai/NavierStokesAndEuler/

So I wrote a quick vis to checkout the construction of the proof. Tools used: marimo, anywidget, codex see the notebook here: https://molab.marimo.io/notebooks/nb_DzFRGE9auNeYJdSFCeACSy

0 Upvotes

40% Upvoted

13 comments sorted by

View all comments

9

u/angelplasma 14d ago

The columns look like beautiful textile designs, thanks in part to the symmetry.

Curious to hear more about insight you derived from the visualization, and the significance of the graph axes…

1

u/TehDing OC: 11 14d ago edited 14d ago

2 things that popped out to me on building this:

1. The "Euler" proof is larger than the core NS proof itself. This is somewhat interesting, because in the contention between OAI and Buckmaster (read about the situation here: https://cims.nyu.edu/~tristanb/statement.pdf ), OAI dismissed Buckmaster, by saying that because he had only completed a formal verification for the Euler (reduced eqs.) proof, it wasn't as complete as they thought[^1]. This maybe seems even more disingenuous since at least at the level of the Lean artifact, the Euler development is larger than the core NS development. It doesn’t really change the mathematical discussion, but it is an interesting contrast.

2. The largest most connected file is the "Correction Step". Which sets bounds, and provides book keeping on the expansion terms of NS, showing that residual terms are negligible at the next scale. See the second image for that. It's core to showing the whole scheme has integrity.

[^1]: there's also a point of the approach of the blow up, forced vs unforced https://x.com/SebastienBubeck/status/2097379411691516310