In building intelligent tutoring systems, it is critical to be able to understand and diagnose student responses in interactive problem solving. We present a novel application of the q-matrix method, an educational data mining technique, to the problem of analyzing formal proofs. Our results indicate that automated analysis of formal proof data can provide an intelligent tutoring system with useful diagnostic information for generating feedback and guiding ITS design.