3 ms·

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

• hgsgm 4y ago
  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.
  • macrolocal 4y ago
    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.
    • ogogmad 4y ago
      > recent progress toward CFT What's this?
      • macrolocal 4y ago
        Buzzard's group at ICL, eg. Ashvni Narayanan.