That's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common

That's not quite true. Many of these proof assistants support some level of automation and proof search. I haven't used Lean specifically, but it's quite common in Coq for projects to write proof search techniques specific to the problem domain and utilize them in their proofs.