On the statement of the classification of finite simple groups.

A widely viewed recent post to MathOverflow by Kevin Buzzard asked the question, "Which mathematical objects would you like to see formally defined in the Lean Theorem Prover?"

Link 1

Link 2

The most highly upvoted response to this question was, "I would like to see the statement of the classification of finite simple groups formalized."  The proof of this classification theorem is one of the largest mathematical achievements of all time.  I will give an expository talk describing the statement of the theorem.  Many (and in some sense most) of the finite simple groups are groups of Lie type.  The classification of finite simple groups is remarkably similar to the classification of simple Lie algebras over the field of complex numbers. This means that the classification theorem has particular meaning for those interested in Lie theory and the structure of semisimple groups.