IMO, syntax is really not the main attraction, neither is it the main problem to solve when writing a theorem prover. Prolog has the advantage of a regular syntax, just like lisp.
Instead of wanting to make your miracle-own-thing, it would be far better to contribute to something like Idris. It's brilliant and in dire need of libraries.
Making formal proving simple and intuitive is the first step to have it heavily adopted. It should look as close as possible to writing a proof in pure first order logic.
I think there's room for a spectrum of theorem provers made for academic pure mathematicians, industry programmers and everything in between. Those should perhaps not have identical syntax, neither should they have the same goals.
To support my point, here's an example of an exotic theorem prover: https://github.com/webyrd/mediKanren It is aimed at medical researchers, and computes proofs about the medical literature, no less! This is a very different system and audience than which you are thinking about, but it's still a theorem prover.
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.
I had a complete opposite reaction to yours. I feel like automatic proving languages are very quirky and stem from the creators not really knowing much about programming. At my university a bunch of professors who really liked Prolog made a formal proving language and guess what syntax it had? Yeah... terrible stuff.
Personally it's been a few years since I started thinking about this matter, but one of my personal objectives in live is to create a decently simple and intuitive (for both mathematicians and programmers) environment for formally proving their theorems