Hmm, is the formal verification through? Lean just asserts no errors in the proof, but like can prerequisites not be fullfilled?

▲

sebzim4500 6 hours ago | parent [-]

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.

▲

JohnKemeny 5 hours ago | parent [-]

It's highly non-trivial to confirm that the theorems written in Lean are actually the same as the Navier–Stokes (non-)theorem.

	▲	sebzim4500 5 hours ago \| parent \| next [-]
		Is it? Clicking around the code it looks like a pretty mechanical translation of the statement on the millennium problem website. Assuming of course that you are willing to trust that e.g. the real numbers definition and API included in MathLib4 is correct, but that feels very safe to me. I'm not claiming to be an expert on Lean4 (although I have contributed tactics) but this is one of the most direct formalisations I've seen of a serious result (second only to FLT of course, which has a horrible proof but it is trivial to verify the statement)
	▲	fpvandoorn 4 hours ago \| parent \| prev [-]
		They actually used Lean statements that were carefully human-written and human-reviewed, from here https://github.com/google-deepmind/formal-conjectures/blob/m... This doesn't guarantee that the statement is correct (Lean cannot do that), but makes it highly likely.