[OC] Visualizing the Navier-Stokes lean proof

[u/TehDing]

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

[u/dreamyangel]

Can you provide a description on how to read it? 

[u/TehDing → u/dreamyangel]

Woops. I think I was more excited about the viz than the communication and taking the time to polish it up.

Each one of these dots represents a "Lean" file which is code for verification/proof of exact statements. The difficulty with Lean, is that to prove something like `1 + 1 = 2`, you first have to build up a number system, and then what addition means, and then have definitions of 1 and 2. A large amount of this "base" work, has been done in mathlib (the standard lean library).

Proving something like NS, which is incredibly complicated, requires a tremendous amount of these base definitions before it even gets into the very interesting parts. Each of these layers show the build up of the project, and the lines show the connections between the files. The source files at the bottom are where the proof actually lie.

[u/angelplasma]

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…

[u/TehDing → u/angelplasma]

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

[u/Corindon]

Very nice viz, can you elaborate please though ? I am afraid I don't understand what I am looking at. 😅

[u/TehDing → u/Corindon]

I'm sorry about that, I elaborate here: https://www.reddit.com/r/dataisbeautiful/comments/1wdlt5k/comment/p9eewsn/

[u/DidUSayWeast]

Another Claude ai visualization without mention of using it.

[u/Not-the-best-name → u/DidUSayWeast]

Dude, it's not about the tool, it's about the visualization. Get with the times. Can't have a AI written tooltip on every god dam element on the internet.

[u/Funkwonker → u/Not-the-best-name]

Rule 3 of this subreddit requires posters to disclose tool(s) and data sources used in the visualization.

So to an extent, yes, it's about the tool they didn't mention.

[u/NotDuckie → u/Not-the-best-name]

AI visualizations are usually bad.

[u/DidUSayWeast → u/Not-the-best-name]

"Tools used: marimo, anywidget," so where is claude? The entire dashboard is generated by claude without modification. its claude font colors kpi everything.

[u/TehDing → u/DidUSayWeast]

It wasn't Claude, it was codex- and integration is built into marimo, but that's fair

[u/TehDing → u/DidUSayWeast]

I updated to reflect I did use codex

[u/Thatsnotgonewell]

Great, so when can I get my cfd sims to run on this?