A Usability Evaluation of Interactive Theorem Provers Using Focus Groups

Bernhard Beckert, Sarah Grebing, and Florian Böhl


The effectiveness of interactive theorem provers (ITPs) increased such that the bottleneck in
the proof process shifted from effectiveness to efficiency. While in principle large theorems
are provable, it takes much effort for the user to interact with the system. A major obstacle
for the user is to understand the proof state in order to guide the prover in successfully
finding a proof. We conducted two focus groups to evaluate the usability of ITPs. We wanted
to evaluate the impact of the gap between the user’s model of the proof and the actual proof
performed by the provers’ strategies. In addition, our goals are to explore which mechanisms
already exist and to develop, based on the existing mechanisms, new mechanisms that help the
user in bridging this gap.