Comment by somesortofthing

It can't consistently produce new, interesting-to-humans conjectures faster than it solves open problems, no. AI-generated natural-language proofs are more or less human-unreadable and are solely concerned with the process of constructing whatever object serves as the counterexample. Natural-language counterparts of formally verified proofs are often unfaithful to the formal component. All of this combines to create less-than-fertile ground for future study.