32

While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson odd-order theorem. Note that the proof in Coq took a team, lead by Georges Gonthier, six years. A large part of this was formalising two books that contain the required material for the odd-order theorem, and its proof.

Are there any efforts, or planned efforts, to take on more large-scale components of the proof of the CFSG?

Candidate results, taken from Wikipedia, include the Brauer–Fowler theorem (which is on par with the odd-order theorem as being foundational for the programme), the signalizer functor theorem, the Trichotomy theorem and the Classical involution theorem. Note that the team developed tools (character theory, Galois theory...) that ideally could be re-used.

Are the components developed for the odd-order theorem able to be ported for other CFSG projects? Or are they too specific?

And finally: anyone like to make a guess at how long such an effort would take? ;-)

Community
  • 1
David Roberts
  • 33,851
  • 6
    How about a formalized proof of the existence of the Monster ;) – Ian Agol Jun 23 '15 at 05:52
  • 1
    The proof of the (fundamental, I agree) Brauer-Fowler Theorem is quite short, and not especially difficult- the key to that result is a great insight. Given that initial insight, the proof can be followed without too much difficulty by specialists. – Geoff Robinson Jun 23 '15 at 07:42
  • 1
    I do not know what is being pursued at present in this area with regard to formal proofs. Long and difficult proofs which I think might be viable candidates, and which are somehow outside the "generic" part of the CFSG proof are the (separate) classification of groups with dihedral and semi-dihedral Sylow $2$-subgroups (low rank Sylow $2$-subgroups in general). – Geoff Robinson Jun 23 '15 at 07:46
  • 4
    This seems the ideal project for computerized proofs. It is a highly cited result that many people take as a black box and which one gets the impressions has skeptics. I am not sure that a computer proof will help the true skeptics but probably some people will sleep slightly better at night knowing that there are both human and computer proofs (I just hope a computer proof wouldn't dissuade people from continuing the revision of the human proof). – Benjamin Steinberg Jun 23 '15 at 16:27
  • 1
    @BenjaminSteinberg actually I would hope that formalising the proof would spur people on to understand and write up the paper proof more - when Hales and crew did a formal proof of Kepler, they had to write a book on the material to pin things down. Likewise, the Coq proof of the 4CT lead to a rethink of the theoretical framework. – David Roberts Jun 24 '15 at 07:23
  • @GeoffRobinson maybe a better term might be 'polish' (now I look it up, I was thinking more of the noun form, and then verbing that) – David Roberts Jun 26 '15 at 06:15
  • 3
    Here is a complementary suggestion. Serre complains that people do not distinguish between theorems conditional on CFSG and those conditional on CFSG+ATLAS. Formalizing the statement and (completely omitted) proof of ATLAS sounds pretty easy to me, but of a very different flavor than formalizing the proof of CFSG (and different is good if your goal is to learn about formal math). Moreover, one should check that the formalization is usable by using it to formally prove conditional theorems. – Ben Wieland Jun 26 '15 at 17:58
  • @BenWieland I asked a question along these lines here: http://mathoverflow.net/questions/215102/how-much-of-the-atlas-of-finite-groups-is-independently-checked-and-or-computer – David Roberts Sep 04 '15 at 05:42

0 Answers0