I honestly don’t think anyone outside of math should care much about these things, for a variety of reasons. I don’t think you should listen much to loud opinions on Reddit, including mine. But if you want to know:

1) The results I had heard of here are pretty impressive — I guess some people are most impressed by the sofic group result, but I personally don’t know much about it so I cannot speak to that. So it’s very strange seeing rabid cheerleading or dismissal by many people on Reddit subs that almost certainly have no clue what a sofic group is…

I’d be pretty impressed if a human came up with the ideas on the results I understand better, as the ones I skimmed seem to reinterpret and then improve classical things in ways I find counterintuitive. They seem to use tools that aren’t super unrelated, but that aren’t obviously useful for the problem either. I’d think a human realizing to use these tools for these applications must have had deep intuition to try this route, but it’s not clear to me that logic applies to LLMs that far exceed us at memorization and brute force. But on the other hand, I feel some sort of weird pride that much of the machinery it uses is in the literature in some form; putting it together and realizing it was useful for these problems is not easy by any means, but there’s something nice about the idea that we built up beautiful tools that seem to have more punch than we realized at the time. I suspect it will still be humans that will digest these new arguments and realize where they may lead to new results for other problems. This has already happened for the unit distance conjecture counterexample.

2) Nobody knows what exactly they do behind the scenes, but they have hired many world-class mathematicians/computer scientists. This is very public information, mostly because part of it was about helping their reputation. They also more or less hired any mathematician that publicly extolled their tools on Twitter last year. My understanding is only some of them are directly involved in these math efforts while others are focused on other things there. Many of them are, though, directly involved in helping generate synthetic data to improve their models at math and code, but I don’t know what this entails exactly beyond ripping ArXiv papers and likely generating synthetic reasoning traces in some way. My vague understanding is also that they run their models all the time on these kinds of problems, and if they seem to produce something promising, some of these mathematicians will take a look to see if it is correct or interesting — that could potentially be used to generate more training data to push it towards more promising directions, but who knows. For this batch of problems, my sense is those mathematicians probably helped rewrite the results into a more readable format and to give more context about the argument as LLMs are still pretty bad at that atm. I would guess the models sketched out the main ideas in some form, and then after checking them, the humans would direct Codex to write better related work and proof ideas and so on like a more human paper. But again, just a guess.

3) The true cost is also unknown but the numbers they give are almost certainly misleading for a variety of reasons. It clearly doesn’t account for the massive compute, synthetic data generation, human input, and so on, that goes into training these models precisely towards improving in these directions. Even for these problems, I suspect whatever number they gave is for the successful runs. But that’s obviously not the same thing as the full cost of them trying their models ad nauseum on all problems and then seeing what worked, which likely took considerable human effort as well. They don’t seem to want to provide any clarity about any aspect of their process, but I do find it hard to believe that they have all these brilliant theoreticians and they work as run-of-the-mill SWEs when they probably hadn’t touched code in years.

4) It’s been clear for over a year now that they have viewed math as a source of relatively cheap PR. Whether or not it’s deserved is up to you depending on how you measure their costs vs. achievements, but they certainly care about the effects on their valuation far more than they care about “advancing science” or whatever. They are shockingly nontransparent about anything, despite only lifting off the ground by promising researchers they would do charitable and open science.