(My apologies for the very slow response; I hadn't noticed your reply until just now. If YGQ doesn't reply to this, future readers should note that the long delay between their last comment and my reply is a sufficient explanation.)
You wrote, earlier:
> For the n'th time: the recent successes of AI in mathematics are the result of a brute-force attack. [...] ~100 GPU years. How many human-years were invested in solving the same problem, before they were overtaken in the last few days by an AI?
I don't see how this makes sense except as a comparison between total AI-agent effort and total human effort. And the result of that comparison is not that the AI agents have put dramatically more effort into attacking the problem than human mathematicians have. Any one of those 10k AI agents has spent a lot less time on Navier-Stokes than a human who's been working hard on it has. All of them collectively have spent less time on Navier-Stokes than the mathematical community at large.
The AIs put an amount of agent-time into the problem that's in something like the same ballpark as the amount of human-time the mathematical community has put in, and (I think) in fact clearly quite a bit smaller. The AIs got to the solution, which the humans hadn't. I don't claim that this makes the AIs more impressive than the humans -- it's plausible that humans were already substantially more than half-way there. But it means that the AIs are at least comparable to the humans when it comes to attacking this sort of problem.
I agree that it doesn't seem like OpenAI's models are as good at mathematics as Grigori Perelman. But a year ago they weren't as good at mathematics as me[1], and a year before that they weren't as good at mathematics as a typical university undergraduate, and a year before that they weren't as good at mathematics as a typical secondary school student. (Don't take any of those timings/levels too seriously; I haven't checked exactly how the progress went. But it's something along those lines.) How do you expect things to stand a year or two from now?
[1] I was an IMO silver medallist[2] and have a mathematics PhD from a good university, but I'm in my fifties and necessarily a bit rusty at this sort of thing, and while I spent a couple of years trying to be a pure mathematics researcher I wasn't terribly good at it and escaped to the Real World.
[2] For those who don't know how it works, this doesn't mean "second place"; they give out a lot of medals of each type. Roughly speaking the proportions nothing:bronze:silver:gold are 6:3:2:1, IIRC. I was a fairly mediocre silver medallist, so maybe somewhere around the 20th percentile of IMO team members worldwide.)
> they look at lot like monkeys on typewriters.
It is hard to take your arguments seriously when you say this sort of thing. 10k monkeys on typewriters, typing one letter per second per monkey, would take something like 300,000 (elapsed) years to get as far as typing "NAVIERSTOKES". (I am assuming typewriters with only letters, case-insensitive.)
The AIs made an amount of progress that was at least broadly comparable to the amount of progress humans had made, with a number of agent-hours of work that was not dramatically greater than the amount humans had taken, to complete the solution of the Navier-Stokes thing. So the AIs were, individually, in something like the same class of ability as the humans.
You may be as impressed or unimpressed by that as you please, of course. You may think it unwise to extrapolate superhuman performance in the future, perhaps e.g. on the grounds that the smarter we try to make them the less relevant training data there is from what humans have done before. You may absolutely have moral or legal or political objections to what the AI companies are doing or what you expect them to do in future. But whatever they are, these systems are a long long long way from being monkeys on typewriters now.