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
“On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems.”
That leaves a lot of ambiguity. Is “result” exclusively “positive result shown here” or “all results”?
Since proving infeasibility is a valuable result, the unpublished problems must not have reached a valuable end state. Thus it’s an operator decision of when to turn the machine off and try another problem. I’d thought they had a three hour time box on this, but apparently not.
For the same reason I'm allowed to draw, paint, or write things very similar to what others have drawn, painted, or written but I have to sign my own name not theirs.
You are a person, LLMs are not. You know this, which is why you know that if you signed someone else's name it would be forgery, but when you see the machine do it you call it a bug.
If the machine is like you, the machine is a forger. The machine is not like you, it is simply blending the work of others to order. Adding someone else's signature is simply part of that statistical process.
I think this is a tangent. The obvious problem with signing someone else's name to work they did not create and do not endorse is that, if you publish the image, you will be falsely attributing authorship to them without their consent. The intent (if any) behind the addition of the signature is a separate issue.
They give up anything that isn't vested and have 90 days to exercise options that have vested. A standard vesting schedule is 4 years and apparently this guy is at 3.5 so yeah he'd be giving some up.
One is allegedly a copyright violation (fair use IMHO but still a grey area legally AIUI), one is a very explicitly a violation of the terms of service you agree to when signing up. And yes I do think that if somebody puts their website behind some barrier where a user has to actively affirm they won't download the contents and use it to train an LLM that should be protected by the same law for the same reason.
Are you arguing that training on copyrighted material is fine but distilling against tos is somehow bad? Lmao what a take. Nah, if copyright cant even be enforced then theres no way on earth violating a tos should ever have repercussions other than they ban you. stop carrying water theyre not gonna pay you
It's so nice of you to think of the poor ignored Terms of Use rather than merely clicking the nag box to proceed like everyone else. Maybe with some more positive attention the Terms might become less depressed, abstain from binge eating, and stop putting on pounds of new paragraphs every year.
