That's fair, but I would argue that reading the specification is very easy by comparison. A quick one hour tutorial is usually enough judging from my students' experiences.
The Lean proof to Fermat's Last Theorem is 13 mil lines.
The one for the quasi-Riemann Hypothesis is half a million.
Indeed! Almost none of these most math folks are likely to read. The only thing to read is the statement, which is only a handful of lines in both cases. The point of Lean is that if that statement compiles and is validated by hand to be equivalent to the natural language statement, then it is true. That was what I was trying to say here.