We describe the integration of permutation group algorithms with proof planning. We consider eight basic questions arising
in computational permutation group theory, for which our code provides both answers and a set of certificates enabling a user,
or an intelligent software system, to provide a full proof of correctness of the answer. To guarantee correctness we use proof
planning techniques, which construct proofs in a human-oriented reasoning style. This gives the human mathematician the necessary
insight into the computed solution, as well as making it feasible to check the solution for relatively large groups.