[wsy]

If you don't _want_ to get a PhD, it will be very hard to finish. It is already hard if you are motivated and eager to do research.

Also, just the title alone is of not much value in industry, you need to have done research in a sought-after area. So if you mainly want to do it for career purposes, interactive theorem proving is probably not a good choice. If you think you need a PhD to get interesting industry jobs, better look for a PhD in an area where FAANG researchers publish.