If this not only verification but generates genuine new proofs, then I might be wrong and have to remove one 'long'. Even then, I am convinced, it will still be a long time until computers can come up with such a complicated proof, involving so many different fields of mathematics, like Fermat's Last Theorem.

Furthermore, math is not just about proving things. Mathematicians invent the consistent formalisms in which the process of proving takes place, and spot isomorphisms between apparently different ones. They also have a knack for choosing to follow paths that will be fruitful, rather than than lose themselves in a maze of pointless symbol manipulation. AFAIK, no computer has ever taken it upon itself to find a proof of some nontrivial issue in mathematics, let alone do any of the less formal things in mathematics.

The issue is that some (actually, most!) of the logics you can reason about are not decidable. So, it is hard to have a sense of progress towards a goal.