7 ms·

Here's the formalization / lean verification: https://github.com/openai/NavierStokesAndEuler https://github.com/openai/NavierStokesAndEuler

• stabbles 9d ago
  341k lines of lean without comments
  • jgbuddy 9d ago
    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
    • frotaur 9d ago
      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.
      • aizk 9d ago
        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.
        • Jblx2 9d ago
          https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
        • frotaur 9d ago
          that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.
  • kzrdude 9d ago
    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/ComparatorChallenges/NavierStokes.lean https://github.com/openai/NavierStokesAndEuler/blob/main/Com... in this case (286 lines).