Generating the lean proof first is a viable approach as well followed by an explanatory pass.

Actually, they are questioning whether the natural language description of the proof is either not faithful to the formal proof, or simply wrong, or both.