The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.

Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.