If writing or generating proofs is hard then the focus should be made on effective search for solutions among proved theorems.
And now there is not a bone in the truck.
sherlocoq didn’t get gathered enough interest and is not running now.
Even built-in search capabilities in Coq among loaded definitions (no tricky indexing is assumed) is very limited.
E.g.
Theorem t1 : forall (a :: nat) (l : list nat), a :: l = [a] ++ l. Admitted.
Theorem t2 : forall (a :: nat) (l : list nat), [a] ++ l = a :: l. Admitted.
Search (_ :: _ = _ ++ _).
Search with the pattern above misses theorem t2 nonetheless it is symmetrical to t1.
Function search by a type signature cannot neglect order of arguments:
Fixpoint f1 (l : list nat) (n : nat) : option nat.
Fixpoint f2 (n : nat) (l : list nat) : option nat.
Search (list _ -> nat -> option _).
So f2 falls out from results.