Comment by mrob

It doesn't matter. The proof verifier is traditional deterministic software with 0% hallucination rate, so any hallucinated proofs are easily removed.