And anyone who's tried to write or read Lean will also tell you that understanding a complicated mathematical proof doesn't necessarily get any easier when it's completely formalised.