It is actually surprisingly fussy to set up a formal proof for anything complex enough to be interesting to a mathematician (for computer assisted verification)

It is actually surprisingly fussy to set up a formal proof for anything complex enough to be interesting to a mathematician (for computer assisted verification). People take big leaps that are often quite awful to actually prove. I think you are right though, this area will definitely be very important and make big strides.