IMO formal theorem proving is the future of mathematics for sure. I've been working on Metamath a bit and basically proving a new theorem reduces to a search problem over the theorems already proven.

In 10 years I think every mathematician will use formal methods, it will be like typing your proofs with a type writer not to. Moreover the problems are very amenable to smart tools assisting in the work, there is a smooth path from where we are now to a fully ai mathematician.