News for hackers. Stuff that matters.

A comment on Navier–Stokes Lost in Translation. Parent comment

Re:Navier–Stokes Lost in Translation by abstrakraft on Wednesday October 07, 2026 @01:01PM (#49995574)
The claim in TFA is that the formalization(in Lean) of the problem does not correspond to the natural language statement of the problem, such that the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
[ Parent | on HN ]
Re:Navier–Stokes Lost in Translation by sigmar on Wednesday October 07, 2026 @01:50PM (#49996281)
>the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".

that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.

[ Parent | on HN ]
Re:Navier–Stokes Lost in Translation by fasterik on Wednesday October 07, 2026 @01:07PM (#49995672)
That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.
[ Parent | on HN ]