Why are theorem provers not more widely used? We briefly discuss some recent case studies we conducted in Isabelle/HOL and HOL Light, especially the mechanisation of a recent research paper in distributed algorithms. This illustrates some general deficiencies in current HOL implementations. In particular, we encounter problems with expressivity and automation.

We describe attempts to address these problems, which involve implementing theory interpretation, implementing sequent style proof terms for HOL, and reconsidering the rôle of automation in an interactive setting.

Time permitting, we will balance the previous description of a difficult mechanisation with that of an easy one, by describing our recent verification of a sound and complete theorem prover for first order logic, inside Isabelle/HOL.