We survey publications that report on the experience of introducing proof assistants into classrooms, identifying observed advantages and challenges. From this, we synthesize a series of design criteria for classroom proof assistants, and suggest methods for evaluating future designs against these criteria. Finally we discuss how we are using these criteria to guide design decisions in ongoing work on designing the Hazel Prover.