One good exercise for students of abstract algebra is to
determine what natural numbers up to some constant can be orders of
finite simple groups. The classification
of finite simple groups categorizes all finite simple groups,
but you can use little more than some fairly basic results such as
the Sylow theorems to determine all numbers less than 1000. This simple OCaml
program automatically applies a few such results, acting as a
simple proof assistant.
