The construction is that there is one file you need read and verify, the challenge file. If you've verified that file and trust that your lean compiler works correctly, the proof will be correct.
The point of lean proofs (as it stands) is simply one bit of information: that a given mathematical statement is indeed true.
It's a way to be absolutely certain (modulo bugs in the lean kernel) that a proof you came up for a statement is indeed correct. It is really not meant to be analyzed, much less now that they are fully llm written.
Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.
The construction is that there is one file you need read and verify, the challenge file. If you've verified that file and trust that your lean compiler works correctly, the proof will be correct.
That file should be https://github.com/openai/NavierStokesAndEuler/blob/main/Com... in this case (286 lines).
Had no idea this was what lean looked like- that's mind blowing. I'm not even sure how someone would critique this if they wanted to
The point of lean proofs (as it stands) is simply one bit of information: that a given mathematical statement is indeed true.
It's a way to be absolutely certain (modulo bugs in the lean kernel) that a proof you came up for a statement is indeed correct. It is really not meant to be analyzed, much less now that they are fully llm written.
Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.
2 replies →