HNHacker News
TopNewBestAskShowJobs

oursland

1 karma · joined July 21, 2026

submissionscomments
oursland··on OpenAI’s Navier-Stokes release included a Lean 4 formal proof
I'm not too familiar with the exact problem as I only became aware of it due to this drama, but I think you're correct. That said, another commenter noted that it may also be one of the Millennium Problems with the least application. We already know "all models are wrong, but some models are useful" (George E. P. Box), the fact that this holds for Navier-Stokes is not a surprise.
oursland··on Codex Security
They're only discovering the security flaws that exist. Would you rather them not be exposed and corrected? To "Slow the testing down"?