[lmm]

If the prover simply went into an infinite loop while checking the first proof candidate and never got as far as checking the second one, would it be working correctly? I would consider such a prover not useful, and a useful prover would be one that told me something when reaching the timeout, such as that there were no proofs for the given theorem shorter than a certain length.

[thamster]

This is handled in university CS algorithms courses. In such a case, dovetailing or interleaving the execution of the TM on the input would be used. Sipser pp. 150–152 https://courses.engr.illinois.edu/cs373/sp2009/lectures/old/...