Document using the Classification of Finite Simple Groups (CFSG) in the algorithms

[hungaborhorvath]

The discussion on this issue has already started in #563 .

In my opinion, application of the Classification of Finite Simple Groups (CFSG) in the different algorithms should be properly documented, to the level of what part of the algorithm uses CFSG, how much the algorithm is dependent on CFSG, and when can an output be considered 100% true, even in the unlikely event if CFSG happened to be false. I would even go that far that at a certain assertion level an InfoWarning should be given to the user about the application of CFSG. Maybe, whether an algorithm uses CFSG or not could affect method selection in some way, as well, maybe as per some user preference?

[stevelinton]

I certainly would oppose the warning and method selection suggestions, and I'm not really keen on the whole idea, though obviously if someone wants to start a documentation project they can.

If the CFSG is not correct (which I think is now very unlikely) it is likely to be through the existence of a 27th sporadic simple group, or, less likely, an infinite series of very large simple groups.

In either case, it is very unlikely to invalidate many of the methods we use, certainly for sizes of arguments that are computationally feasible this century. For instance the existence of a new sporadic group with no permutation or matrix representations that can be written down in less than 10^30 bytes is unlikely to change the result of any computation anyone will ever do.

So if we raise a warning for someone computing with groups of order 10^9 that some result "depends on the classification" we would be misleading them. It can almost certainly be checked using only a tiny fracton of the proof of the classification, but huge and essentially pointless effort would be needed to work out what fraction in each case.

[markuspf]

I'll repeat/add to my comments on #563.

I am not sure whether displaying a warning relating to CFSG is useful, because after all, we'd have to also start displaying other warnings: oh, this group is soluble because it's order is odd? Even though the odd-order-theorem has been machine verified, this theorem could have flaws.

I think it is more likely to find bugs like the recent bug in semidirect product code than bugs in theorems that are widely known and put into mathematical contexts in many ways.

Documenting whether the CFSG is used is probably a nice piece of documentation work.

[hungaborhorvath]

About the Feit-Thompshon theorem: as far as I understand, there is no question about this among mathematicians, this is a complete and clear proof, even if most of us will never get the chance to fully understand it. In other words, this is a completely accepted theorem in the mathematician community.

This is not entirely the same with the classification. While I do not know if anybody explicitly doubts its results, or its proof, I know that it is still a common habit to document in a paper how exactly the results of the paper rely on the classification. The most recent I know about is Babai's subexponential theorem on the graph-isomorphism, and he very clearly pointed out in both the manuscript and in his algebra talk which are the parts of his proof and algorithm that use the classification and in exactly what sense. He even spent a couple minutes explaining that one of such dependence has been since eliminated by Pyber in the expense of a couple of additional log factors in the exponent.

About the documentation, I would not want it to be too much. I am rather sure that a lot of algorithms do not use it explicitly. (In fact, I have not yet read code in the library where I have observed that this is used. I read only an immediate method about solvability using Feit-Thompson, and that actually is documented in the manual.) I would rather think that a page on the GAP webpage could be devoted to this, where one would put up that e.g. NormalSubgroups uses the classification where it does this and this, etc. Just some explanation in a couple sentences, obviously for people who understand what it is about. And maybe write the potential situations where this might result in bad computations, if that at all is the case. Maybe I am overly naive, but I was surprised when @hulpke mentioned that NormalSubgroups uses CFSG to some extent. I would be interested in what capacity does it depend on it.

BTW, for me it is very hard for a lot of algorithms to find what paper they are based on. Maybe I am not looking at the right place, but as an example: for polycyclic groups (which seems to me one of the more important implementations for GAP) I did not find any papers mentioned on pages 45 or 46 of the manual, and only yesterday found one of the basic papers by the nth google search.

[fingolfin]

I do think it is a good idea to document for more algorithms on which papers they are based, and I wouldn't mind if this also includes a remark pointing out that the CFSG is used. But IMHO it is sufficient to have this in source comments and/or manual entries.

Overall, I am not worried a bit about the correctness of the CFSG, at least in as much as it concerns actual computations we can perform today -- for the reasons @stevelinton already explained. However, I am concerned about code which implements algorithsm I do not recognize, and for which I cannot find out on what paper they are based.

BTW, finding papers via google is usually a futile effort. Use databases like MathSciNet or Zentralblatt instead.

[frankluebeck]

I support the idea to have more documentation of non-trivial methods with citations of the relevant literature. Mentioning that a certain algorithm uses CFSG sounds sensible, although I agree with @stevelinton that in most practical computations only (often trivial) parts of the classification are really needed. Therefore, I also disagree with the idea of raising warnings in case an algorithm uses CFSG.