> simply dumping proofs on the math community and expecting others to do the grunt work of verifying, refining, and expanding on them is hardly a productive way to advance the field.

I tend to agree with this, but what is the alternative? Should OpenAI and Anthropic employ hundreds of mathematicians to do this work? Should they just not solve math problems within their reach?

I tend to disagree with OP, for the same reason.

It's unclear what more could be expected than releasing the presumably already verified results and write-ups for each problem. Should they run a mathematics school too?

Then the comment goes on to argue AI labs were not interested in actually advancing mathematics, and that investments into AI were manically excessive.

IMO none of this follows and demand is there to justify the investments.

The comment then goes further to argue that AI labs were putting too much effort into pretending there was exponential progress rather than actually making progress.

The factual basis for this claim seems to be that OpenAI released math results and write-ups, and it's not even clear what more they could do on that topic.

That's a very negative opinion.

Look at how actual researchers are currently using the tools: they'll generally use the LLMs to create slop papers, sometimes supported by auto-formalizations, just like OpenAI does. Then they will go through the lengthy process of digesting the results, turning the often incomprehensible and poorly organised outputs into something that humans can understand and build upon, they will then give seminars on the results, further helping with dissemination. Doing so still requires expertise, and probably will for a good while.

So yes, that is exactly what they should do. Alternatively, if they are too lazy or incompetent to put in the effort themselves, do what AGMAI proposed and fund a third party to help out.