The output would be a string containing the proof, which a deterministic, non-LLM proof-checker could decide whether it’s correct or not.

This part seems like an optimistic statement. Do we have LLMs outputting proofs in a consistently correct format that prof checkers can accept?