As bureaucracies look at AI and staffing, this is going to be the headline in the executive summary.
Sure yeah, today it's only a 5% solution (to the hardest problems), and we know it will top out somewhere.
But the cost reduction is just too good to ignore.
Terry Tao was saying that we need more mathematicians [0]. My paraphrase of his article is that we will need them to check the AIs, essentially (I missed things didn't I?).
But with a near 10,000X reduction in cost [1] today, it's really hard to argue for that when budgets are continuously tight.
[1] assume ~$150k/year for a mathematician of the caliber that can do this work. 2x that for overhead like healthcare, 401k, etc. Do this for 35 years of work = $10,500,000. Assume about 1 result of this caliber per mathematician. So ~$10M per result. OpenAi is saying they can do it for ~$1k, a 10^4 X decrease.
You're off by an order of magnitude at least. A mathematician does much more than just prove theorems. Let's start by teaching and administration duties.
And then you're off an order of magnitude of the efficacy of OpenAI. We don't know how much work of mathematicians is behind all these results, what's the real cost (which includes those problems they couldn't solve), etc.
Oh I entirely agree! Mathematicians are full human beings.
But a soulless admin is not.
And they care only about the budget.
And the real danger here is that these large groups of blame avoidance mechanisms take at best half a look at the cost of an AI and the cost of a pre tenure track new assistant professor (or whatever), and they decide, oh maybe next year we can hire someone.
I think it's not just to check - it's to interpret, simplify, apply taste, basically get these proofs into a form that humans can grok and build on. AI could do all of that but the grok-ing -- as we are tapping the font of cheap proofs it still behooves humans to keep track of what we find interesting, keep internalizing and learning concepts and make sure whatever we're building right now will be generationally useful. At least that's my take
>I think it's not just to check - it's to interpret, simplify, apply taste, basically get these proofs into a form that humans can grok and build on.
Sure, but we are approaching a time at which we will have to answer a "why" here. I.e. anything beyond checking and validation becomes of mostly artistic value at some point. And there is nothing wrong with that.
IMHO it's groking that allows higher level metaphors and eventually more powerful theories to be built. If all you are doing is proving everything reachable by construction, you aren't really learning, as this process won't be drawn to the more compressed expressions by necessity but only as a "please" from the humans.
I’d say the artistic value is the main value in general —- if you know mathematicians they will often refer to a ‘beautiful’ proof, aesthetics is a critical part of math.
An early (easy to understand) proof that fits the bill for me is proof that the sqrt(2) is irrational: a very natural thing to think about —- for a unit square, what is the measure of the diagonal? And people were killed in ancient Greece over the proof, but it’s comprehensible with basic algebra.
If we have a jagged frontier inside the domain of math (very plausible, the jagged frontier concept seems to be quite fractal), the model solved the easier problems in his area of major strenght, some of them will be in the bottom 5% of the easiest problems in the full set, and some in remaining 95% of problems
Sure yeah, today it's only a 5% solution (to the hardest problems), and we know it will top out somewhere.
But the cost reduction is just too good to ignore.
Terry Tao was saying that we need more mathematicians [0]. My paraphrase of his article is that we will need them to check the AIs, essentially (I missed things didn't I?).
But with a near 10,000X reduction in cost [1] today, it's really hard to argue for that when budgets are continuously tight.
[0] https://terrytao.wordpress.com/2026/09/24/were-gonna-need-a-...
[1] assume ~$150k/year for a mathematician of the caliber that can do this work. 2x that for overhead like healthcare, 401k, etc. Do this for 35 years of work = $10,500,000. Assume about 1 result of this caliber per mathematician. So ~$10M per result. OpenAi is saying they can do it for ~$1k, a 10^4 X decrease.