[ummonk]

This sounds like a no brainer. If you don't actually enjoy academia then it definitely isn't worth it; even for those who do enjoy academia, a PhD is hit or miss.

You can go into industry and work in that time, and you'll have at least as interesting a life at the end of it. And if industry demand for interactive theorem proving does increase (which it would have needed to for you to get a job in it at the end of a PhD), you will have ample opportunity to learn it on the job instead of in school.