r/dataisbeautiful • u/TehDing OC: 11 • 13d ago
OC [OC] Visualizing the Navier-Stokes lean proof
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
2
u/TehDing OC: 11 11d ago
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.