"But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time."

Unfortunately in my experience that's not really the case. For me, very often GPT 5.5 (which was a good deal better than Opus at this kind of task) would just get stuck for long periods when working in a logic like Iris. It wouldn't necessarily outright prove nonsense, but it would vastly overclaim what it had proved and failed to get anywhere without a lot of hinting. 5.6 is hopefully a lot better about this.