Carlos Simpson, in the nineties wrote "Descente pour les n-champs" together with Andre Hirschowitz. Apparently they were quite ahead of their time: No one could be found to referee their paper. So to know whether it is correct or not, Simpson started developing an automatic theorem-checking program for category theoretical statements. Later it turned out that there was a small inaccuracy (they used covers where they needed hypercovers), but I don't know if it was found by help of the program...
Anyway it clearly shows how it can be useful.