I'm not sure the question is real an MO question, but I'll bite; the three greatest obstacles are:

• a theorems database (that's the easiest one)

• a reasonable algorithm which can bridge trivial steps (they are trying to build one for years)

• a reasonable language (the closest you have is Mizar, and it's very far from the way we write math)

In the current state of afairs, I don't think they are usefull even as proof verifiers, let alone proof assistants (I'm not refering to CASs - but to auto-proof verifiers).