Comment by infogulch

The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.

That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.