I have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.

Most mathematicians don't care about being exactly right. They only need to not see a contradiction. Since most pure math is not used for anything except more math, mistakes rarely have consequences.

A computer is only a threat, that might find a mistake that humans miss.

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.

> recent progress toward CFT

What's this?

Buzzard's group at ICL, eg. Ashvni Narayanan.

Some steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)