To spell out all the logical details of a proof, as required by a theorem-prover, can be routine — not very illuminating, even boring. The HOL theorem-prover provides various rewrite tactics and simplification sets to ease the task, but picking out the appropriate tools to do the job still needs experience.
However, sometimes you’ll hit a stumbling block: something that looks simple and must be true, but you just can’t see any simple proof of it. That’s when the proof becomes interesting.
This is not related to a particular theorem prover. Ask any mathematician and he or she will tell you stories.
The solution of the “stumbling block” usually involves a key idea.
For example, given a number N, how to show that there is a prime greater than N? There is no known formula to generate primes. It was Euclid, around 300 BC, who recorded this key idea: use N to generate a number M such that M cannot be divided by any primes up to N. By case-analysis of this M, the infinitude of primes can be proved.
Of course, during case-analysis of M, you’ll need to show that any number must be a product of primes. If this is a stumbling block, you’ll need another key idea. And so on.
How to find the key idea? Using examples or pictures can help visualizing the stumbling block. After some deep thoughts, the key idea will dawn upon. Sometimes you need to look outside the box. And you’ll need pencil-and-paper to try out the key idea, as the theorem prover will not allow unproven stuff.
To find the key idea in a proof is almost an art — there is no algorithm for it.