I was thinking something along the lines of making a mistake when inputing the initial statement, like you wanted to prove that '2 is even' but what you actually stated was that '3 is odd'.
replyOf course in this simple example it's obvious, but my assumption was that these machine generated lean proofs are millions of lines of code and who knows what they actually say..
You're correct that nobody really understands what these huge Lean proofs actually say. However, the initial statement, even for Navier-Stokes, is not very long [0]. Still, you are also right that sometimes the problem statement can be wrong but it is highly unlikely here.
reply[0] https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
One wrench to throw into this is that there are a lot of bugs around Lean and they have been incidentally exploited in the past. Hence, we still need a level of human verification today.
reply