I don't recommend doing PhD in "theorem proving" as I don't see a lot of industry demand for it. Machine learning, statistics, optimisation, ... all better choices (if you know you're not going to stay in academia).

Having said that, I'd apply for PhDs in other countries as well. Hopefully some would offer you a place directly, not "1 year of free work that will potentially (a.k.a. "not") lead to a PhD opportunity".