They published both a natural language proof and a lean proof. This paper says the NL proof does not match does not match the lean proof, using different arguments and some stronger claims. It does not claim the lean formulation of NS or the rest of the lean proof is invalid.

"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."