We need to develope tools that can automatically fill small gaps (ones left as errors in the essay), because the point of having mechanized proofs is to not have gaps. Then practitioners can write lemmas and let the computers do the checking.
In the proof assistants I'm familiar with, such as Lean and Coq, you can write tactics which generate proofs for a goal and potentially produce more subgoals. However there isn't a "one size fits all" tactic for these gaps.
One area that is being explored is ML for generating proofs, but training data is limited.
The tactics still require users to be aware of their existence and using them correctly (a non trivial mental load). And the resulting proof script is brittle and hard to read. This is what the essay attempted to improve over.
Automated tools like Sledgehammer (Isabell/HOL) removes a lot of the manual work.
I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.
I am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.
Dafny is a great example of what you are talking about. It automated most of the proving. However you still need to figure out the key invariants.