This (ahem) contradicts my experience. Most mathematicians I’ve met are excited about formal verification, especially the recent progress toward CFT.

Thompson himself has said he’d like his contributions to the classification of finite simple groups verified in his lifetime, and actively followed/encouraged the Coq implementation of his odd order theorem back in 2012.