>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.

That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.