[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").