> What’s not clear is whether the juice is worth the squeeze: will all the money spent on spamming the AI and human mathematician time spent studying the outputs progress the field “better” than without the AI?

The AI proofs are a side-product of benchmarking current and in-development models on especially hard problems. They're clearly cost effective for frontier AI firms, and free for the taking as far as human mathematicians are concerned. The real issue with them is that they look like bizarre nonsense as written, so they need mathematicians familiar with those specific areas of math to "decode" and digest them.