3 ms·
Is there a proof here at all? The only thing mentioned in the article is a computation. With due respect, computer-readable proofs are not very interesting to
by mik1998 4y ago
Is there a proof here at all? The only thing mentioned in the article is a computation.
With due respect, computer-readable proofs are not very interesting to me as a mathematician. I don't see why we should do it. Reproducibility is not a concern.
- anonymoushn 4y agoSome steps of the proof are left out. In particular, the correctness of the computation for its purpose is omitted :)
- macrolocal 4y agoI have trouble imagining a mathematician wouldn’t welcome formal verification of eg. the classification of finite simple groups.
- hgsgm 4y agoMost 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 agoThis (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 agoBuzzard's group at ICL, eg. Ashvni Narayanan.