Within the context of theorem-proving, that's not as significant a problem -- you still have a verification of the proof at the end. The value of AI is that it could potentially replace human intuition for how to construct the proof. Humans don't always get this right either. It may take the AI many attempts to get the program right, but you'll know at the end that it is correct.