Re:Navier–Stokes Lost in Translation
by tempfile on Thursday October 08, 2026 @07:42AM
(#50004645)
> No one is disputing that the Lean formalization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?
Re:Navier–Stokes Lost in Translation
by Ohentis on Thursday October 08, 2026 @10:24AM
(#50006201)
Well the theorum statement (what it proves) is short and easy to verify. I would not be surprised if hundreds of mathematicians have looked at it at this point.
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?