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.
The Lean proof to Fermat's Last Theorem is 13 mil lines.
The one for the quasi-Riemann Hypothesis is half a million.