[emileokada]

A lot of proofs at masters level and beyond omit a lot of details because they can easily be checked, but would be tedious to write out explicitly. This means that a 1 page proof would probably actually correspond to 2-3 pages (or more!) if written out with all the details (e.g. with standard but tedious arguments fleshed out properly, and all cases delt with explicitly (rather than resorting to a 'and the other cases follow through similarly' remark)). When written in a proof assistant this would become even longer because natural language allows us to brush a lot details under the carpet because they are understood from context.

[chriswarbo]

A great example of how tedious it is to list out all the steps of a proof is the Principia Mathematica https://en.wikipedia.org/wiki/Principia_Mathematica

"Proof assistants" like Coq and Isabelle can generate some of the more "obvious" steps using metaprogramming (known as "tactics").