Comment by somesortofthing

Strip mining interesting conjectures. AI can answer interesting(pedagogically valuable, carrying important implications, etc.) mathematical questions in formally correct gibberish far faster than mathematicians can generate them. Until AI can replace the conjectures it resolves on its own, it's consuming a finite resource.