6 ms·

the proofs were verified in Lean, so unlikely.

• nicce 8d ago
  As long as the proofs itself are correct. How long they were this time? Edit: at least ~600,000 lines https://stanfordtechreview.com/articles/openai-buckmaster-navier-stokes-lean-proofs https://stanfordtechreview.com/articles/openai-buckmaster-na...
  • latent-person 8d ago
    To claim something verified in Lean is wrong, you need to either argue that the theorem was stated incorrectly, or that there is a bug in Lean (assuming no `sorry` etc, which is checked by comparator). The number of lines needed to prove it is irrelevant (other than checking for a bug in Lean gets harder).
    • nicce 8d ago
      That is the point. Someone must verify that the Lean matches the actual theorem, precisely as it should be interpreted.
      • latent-person 8d ago
        Which has nothing to do with the total number of lines, it's just the theorem statement you need to check. Here is what they showed, which is under 300 lines with comments https://github.com/openai/NavierStokesAndEuler/blob/main/ComparatorChallenges/NavierStokes.lean https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
        • nicce 8d ago
          That seems to be indeed true. I guess it gets validated quite soon.
• thesz 8d ago
  But still possible [1]. [1] https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...