> is there some clear step that (for example) shows a proposition, which might be laborious and hence omitted normally, and is not amenable to being automatical

> is there some clear step that (for example) shows a proposition, which might be laborious and hence omitted normally, and is not amenable to being automatically filled in? Automation works well for first-order logics, whilst proof assistants work with higher-order logics. One consequence is that inductive proofs are very difficult to automate; we can say "XYZ follows by induction", but the computer's often unable to construct such a proof. There are various approaches to converting back-and-forth between different logics, eg. Isabelle's "Sledgehammer" tool, but - Some structure can be lost or obscured in the initial translation, which makes finding a proof harder - Using proofs converted from another logic can cause proofs to be overly-complicated and "unnatural". If they have any computational content (eg. where the proof is a datastructure or function), this can make working with such values more difficult (eg. if we want to prove a property holds in every branch of a function, having an overly-complicated function which branches based on not-completely-relevant conditions makes our life harder).