From the point of view of formal math, what would constitute an appropriate statement of the classification of finite simple groups? As I understand it, the classification enumerates 18 infinite families and 26 sporadic groups and asserts that a finite group is simple iff it is in one of these families. Now the 18 infinite families are all fairly clearly defined as cyclic groups, permutation groups, matrix groups over finite fields, etc. so I don't think there is much difficulty in defining these precisely. Much more problematic are the sporadic groups, which are "known" and hence apparently need no definition.
To give an example, since the monster group is some finite object we could just write down its Cayley table and define that to be the monster group. There are two big problems with this: (1) this table is huge and redundant, and (2) it's not easy to work with this table to prove properties of it. The main problem is that we don't think about the monster group in terms of its Cayley table, nor even as the group generated by a certain pair of $196882^2$ matrices. Instead we view it as a specific group which satisfies some properties and is uniquely defined by those properties; presumably it is in this context that a given sporadic group will show up in the course of the classification proof.
My problem is that I have no idea what those characterizing properties are. Indeed under some definitions it would rather weaken or trivialize the statement of classification, for example if I defined the sporadic groups as the simple groups that are not in the 18 families. What definition of these objects is actually used in the proof?
(Side question: 16 of the 18 families are usually collected under one label, the "groups of Lie type". Is this class definable in some uniform way, or are the definitions individualized and the name is just due to some commonalities we recognize between these families?)