  Large language models have the potential to simplify formal theorem proving
and make it more accessible. But how to get the most out of these models is
still an open question. To answer this question, we take a step back and
explore the failure cases of these models using common prompting-based
techniques. Our talk will discuss these failure cases and what they can teach
us about how to get more out of these models.
