Not a mathematician, but "pretty sure" might not be good enough to resolve this question.

Lucky that it was enough in this case. The theorem had been written by formal conjectures before the proof https://github.com/openai/NavierStokesAndEuler/blob/main/Com...