Proof steps can become different in Lean but still work to prove the theorem. Incorrect proof steps in the NL paper could also be converted to correct ones in Lean. The paper shows some examples of this. So the NL paper can't be trusted even if Lean verification passes, but it doesn't immediately mean that the NL proof is wrong or that Lean is checking the wrong thing.