It's not really the syntax but rather that until very recently theorem provers have been quite niche even in formal disciplines, so the tooling isn't quite there.

In an analogy with traditional programming I'd say we have goto but we are yet to have structured loops. Enormously powerful but still hard to apply to either real mathematics or real problem.