There are an astronomical number of true theorems, but almost all of them are uninteresting and not useful. We've had automatic theorem-generating software for

There are an astronomical number of true theorems, but almost all of them are uninteresting and not useful. We've had automatic theorem-generating software for decades, and there are so many useless true theorems that it can keep busy with all the CPU cycles you throw at it without necessarily generating anything useful at all. Even if you let it run with huge resources and generated loads of theorems, searching through them seems pretty hopeless. Where machine learning systems like LLMs may be able to help is to spot analogies and ways to translate theorems to different areas to do something useful (but the tendency to hallucinate seems a formidable obstacle for things that must be proven). For real automated headway/assistance, I think we need something like Alpha Go's "intuition" at judging the value of a board state somehow applied to mathematical arguments. That's how mathematicians usually work; we have an intuition that we can use a particular approach to prove something, and then we fill in the precise particulars.