5 ms·

341k lines of lean without comments

• jgbuddy 8d 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 8d 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 8d 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 8d ago
        https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
      • frotaur 8d ago
        that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.
• kzrdude 8d 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).