They should feed it the classification of finite simple groups and get it to simplify it/turn it more constructive.