Computer algebra systems such as GAP and Maple can be used to provide the necessary witnesses for applying the criterion. The medium used for communication between these systems is the OpenMath language.
The formalization in Coq is interesting because we were forced to prove a large amount of trivial and less trivial results which are usually not explicitly mentioned in the informal proof. It is clear after this experiment that still a lot of work needs to be done before one is able to reach the conciseness of informal mathematics.
If time permits, I will give a short system demo.