By "it" people in such cases are usually referring to the NL proof. It seems nobody has any hope of undersanding AI-generated Lean code any more, if only due to volume.