The proof is about one of a multitude of possible theorems you could prove about the Navier-Stokes equation. Nobody is claiming that the Navier-Stokes equation itself is misformalized. Rather, they are claiming that what the theorem they proved says about Navier-Stokes is misformalized, in the sense that it's a different theorem than the one informally proven in the natural-language proof.
But nobody is claiming that it's a theorem about a misformalization of the Navier-Stokes equation rather than about the Navier-Stokes equation itself, and nobody is claiming that the theorem they proved in L∃∀N isn't proven. Except random ignorant commenters on Hacker News.
I don't know why this is so difficult. It seems like a lot of commenters here have the reasoning ability of GPT-3, possibly because they're extremely drunk or sleep-deprived, or are actually GPT-3.
But nobody is claiming that it's a theorem about a misformalization of the Navier-Stokes equation rather than about the Navier-Stokes equation itself, and nobody is claiming that the theorem they proved in L∃∀N isn't proven. Except random ignorant commenters on Hacker News.
I don't know why this is so difficult. It seems like a lot of commenters here have the reasoning ability of GPT-3, possibly because they're extremely drunk or sleep-deprived, or are actually GPT-3.