> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!
Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document