alt Hacker NewsAre you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.
Are you asking if it uses additional axioms of `sorry` in the proof? It's easy to check that it doesn't by compiling it and telling lean to list the axioms.
It's highly non-trivial to confirm that the theorems written in Lean are actually the same as the Navier–Stokes (non-)theorem.