I am not from the math field, but heard a couple of days ago a talk in which Lean was part of it. As far as I understand Lean is used to proof assist these theorems (please correction my wording, if necessary) which is also mentioned in the text. As an AI skeptic I still am with you, we need to proofread it. Therefore I would like to know how much of an assistance Lean is in these proofs.