I wonder if top labs will soon abandon math progress like they did go and chess.
In example of go where I'm more familiar Google deep mind poured large resources to get a super human performance first, establish superiority and abandon it. The community then built their own tools starting from reproducing their papers.
I think similar thing might happen to math. Nobody outside of math cares too much about Hamiltonian cycles in some bizarre graphs or proving lower bounds on complexity of some problem.
Once those results stop being worthy of mainstream media attention, they will abandon math and the progress will be done by mathemicians guiding the models and the community will likely establish some new rules about what makes a valuable contribution. Merely solving not yet solved problem might not be it anymore.
The amount of money they're lately ploughing into proving math theorems is inconsistent with how societies and markets have priced pure mathematics. The entire US federal budget for math research is something like $100M annually. A single college football coach can already earn 10 percent of that.
Pretty much the only enterprise that historically pays some mathematicians handsomely is quant finance, but those people are actually compensated not for proving theorems but rather for statistical modeling and programming skills. And even that industry is so technologically driven these days that pure research mathematicians no longer hold a clear edge over strong programmers with undergrad level probability and statistics at their fingertips.
Math is one of the most verifiable domains, esp thanks to LEAN, which also build coding skills.
The $$$ they're pouring isn't just for marketing. Think of these papers/results more as "useful side effects" from large-scale RL rollouts and post-training. Every token being generated contributes to post-training in some way.
There isn't a hard boundary between "training" or "inference", modern post-training is arguably inference-bound :)
It was shown quite some time ago that training LLMs on programming tasks improves their logical reasoning skills also in other natural language domains. So I could see math also being a training gym for AI even if the final use case is not directly math-related. Having to solve math problems efficiently can build in skills that come handy in all kinds of more everyday tasks or science and engineering.
It’s also very useful signal that the reasoning trace is leading to solving open problems - you can be certain that you’re not landing somewhere inside the training data.
I think the entire thing here is that these solutions _are_ inherently interpolations of existing work in the field. That's the "super power" that LLMs have. To interpolate mass amounts of multi-dimensional data.
This depends on some handwavy use of the term "interpolation", not the mathematical definition. Mathematically interpolation usually means that the query point is in the convex hull of the data points, and that almost never happens in high-dimensional spaces.
See:
Learning in High Dimension Always Amounts to Extrapolation
Randall Balestriero, Jerome Pesenti, Yann LeCun
https://arxiv.org/abs/2110.09485
I guess you mean by "interpolation" that it's some kind of nonlinear combination of the training data, but that's an almost vacuous statement. Any input-output relationship has to be so by definition.
Or perhaps you mean that interpolation is when the test input comes from the same distribution as the training input (though this is not technically the meaning of "interpolation"). But this is also quite difficult to pin down.
A lot of people have been surprised by the interest that AI companies have in solving maths problems without obvious applications, as well as in the financially precarious state of these companies. I imagine that they thought that these companies were helmed by mere bean-counters, like at Boeing. But no, I reckon that they're still academics at heart, and so they work on Navier-Stokes and L=BPL, instead of on how to maximise value for their (soon to be) shareholders.
No, more like the average can be more important than some outlier's impact, at least for steady progress. So while you do need the Mozart and Einstein, a more productive effort would be to raise the general population's education level.
Humans learn in the side effect of education, nobody is busting out some poor method that schools teach to solve antiquated problems in the real world.
I don't think it will be the case, maths have real utility. I found something interesting at the intersection of combinatorics and information geometry. To be quite frank I don't understand what I'm doing. And yet, when I ask ChatGPT to use the framework we're developing to write an algorithm, it turns out it has quasi-parity with the state of the art. I have to measure absolute perfs to decide which one is better – theirs, not mine. Ok. Time to keep improving on what I have. And this implies dropping the code and going back to the blackboard doing more super abstract math that are way out of my league.
We are at the point where the way in which humans do math and science changes significantly, and I have no good idea at all in what state is it going to settle down. But you are one of (many, I suppose) people exploring the new wilderness, so I wish you best.
If we get AI singularity, then humans will stop doing scientific progress altogether. But if we don't, then it's pretty predictable what's going to happen - things will be much the same as now, except everyone will be using AI for proofs, data analysis, theoretical models and designing experiments, so important discoveries will happen more often. It's also possible that after the AI craze dies down, we'll have enough computational capacity to solve protein folding.
Some math has almost incalculable business value, because math is the biggest driver of game-changer technology.
We'd be nowhere without Laplace and Fourier transforms, Maxwell's equations, elliptic curve cryptography, and many more.
Most math doesn't, but often these techniques are invented first and the applications come later.
And the criticism of the current round of proofs is that while they may be true - likely for some, questionable for others - they're not adding new techniques or insights.
Why do you think this has no business value? It would be absolutely wasteful for OpenAI to not be doing this as part of a post-training RL rollout.
There are architectural advancements yes, but lots of progress from LLMs really come from (1) better pre-training [generally through more cleaned data, and ofc more data], and (2) lots and lots of post-training. It's how we get more and more intelligent models for the same param sizes.
The 'marketing' is just a useful side effect they get from their RL rollouts on maths and LEAN.
There is a risk of this particularly if it's seen as advertising - at some point "ai model solves hard to explain problem" isn't going to be news and that benefit goes.
However, there's some of this that's a proxy - the compute to solve these problems was very low (they claim a few hours of thinking time on a regular subscription). The large cost would have been the training and if training the models to be better at these things makes them smarter for useful tasks that's beneficial. I believe there was work done earlier on around showing that training the models on code made them better at broader reasoning tasks (not just writing the code itself).
Another side is that if one goal is to improve the models themselves, their ability to work on mathsy problems must be high. That has very direct business value, and ideological value depending on what you think the motivations of the people running the companies are.
Yeah chess is a good example. DeepMind came for publicity with AlphaZero. Arranged a match with Stockfish with rigged rules to make AlphaZero look better than it really was (it was amazing but the match wasn't fair) and then just published some games and went home.
I was bitter about that back in the day as I hoped for more answers, more matches, more "truth" about chess being shown. Soon after that community project Leela Chess Zero was started and not only surpassed original AlphaZero but added few hundred ELO points over it. Then the combination of NN and classical engines happened with NNUE and current Stockfish is again a few hundred ELO points stronger.
Today we pretty much know the truth in chess for all practical purposes. Human analysts/preparation experts focus on finding interesting path and opponent profiling (what is the most unpleasant for the opponent to face). They don't look for truth anymore. The game is doing great, it's more popular than it ever was.
Stockfish and other classical engines were never intended to be run in matches without opening books (of which there were plenty).
Development assumed the presence of opening book and authors made 0 effort to make engines play well in openings because of it.
This is also the reason classical Stockfish was a very small binary. A little effort to make it even by including even a very small opening book (like 50MB or something that would result in still smaller binary than NN engine with its net) would make it much more interesting.
The result was that Stockfish lost many games by walking into known bad lines and lost way more games than it otherwise would.
> We also played a match that started from the set of opening positions used in the 2016 TCEC world championship, along with a series of additional matches against the most recent development version of Stockfish, and a variant of Stockfish that uses a strong opening book. In all matches, AlphaZero won.
Ok I remember it vaguely but the match that got publicity and the one published results were derived from was 1000 games match from starting position.
Deepmind claimed AlphaZero also won from TCEC positions and vs Stockfish with good opening book but at least back in the day I don't think I could find those games being published or specifics about books/positions they have used. Can you?
I am not claiming AlphaZero wasn't stronger. It wasn't as strong as the PR piece suggested though and we have never seen the games being published. In chess this is extraordinary because basically all games in chess are publicly available - both human and computer games.
Claiming "we have created a strong engine that has beaten Stockfish with opening book" while not showing those games (or details about opening book used) is akin to "we solved this math conjecture" without showing any kind of proof or argument.
Publishing a few 1000 of games costs nothing. Tens/hundreds of thousands of games are published every day.
> I wonder if top labs will soon abandon math progress like they did go and chess.
I definitely think that this is marketing, just "with good side effects". My doubt is when they will be able to move to "marketing with better side effects", that is, research with more concrete outcomes (health, materials etc.).
While top AI labs no longer focus on chess, the community build way better chess engines.
Stockfish is probably stronger, than everything the top labs build.
Wouldn't we expect the same thing for math? That slowly the broader math community would engineer a harness/program... That will surpass the current labs, and be a community ran project
Yeah its certainly true now that Stockfish is much stronger than alphazero, but it's probably also true that had Deepmind spent another few years working on alphazero it would be enormously stronger than either.
In the case of chess this seems fine, there isn't much value to society in creating an AI capable of beating top humans with a 4 pawn handicap rather than a 2 pawn one, but for maths where there are actual applications it is more complicated.
They aren't trying to 'solve' chess, go, or mathematical proofs as an end in themselves, but mainly in order to learn more about how to build better systems overall. The goal of AlphaZero was ultimately as a stepping stone towards AGI, and it's the same with LLMs.
That’s still an assumption. Since when do you uncritically believe what people are saying without taking into account the different external drivers on those people.
You can believe they believe they are telling the truth or that they have good intentions while still being skeptical of the effective trajectory.
This misses the raw advantage of a good proof. It makes conceptualization simpler. In some ways math is like a hash list of of theorems. This list makes it simpler to prove other calculations, and will always be useful, to both humans and AI models. I can see two new directions 1 - the creation of specialist theorem models; that can answer questions efficiently about one topic and 2 - we probably need to incentivize and codify ownership of theorems; charging a proportion of the compute saved by using them. Ultimately enabling mathematicians to be paid our true market value!
Oh boy, please not 2. What if this was a thing already and, since neither Newton nor Liebnitz had kids, we all had to pay some investors who bought the rights to calculus every time we took a derivative.
I wonder if it makes conceptualization simpler for models too, given that they're trained already on human-speak. And I'm also curious as to whether humans currently have an innate advantage into simplifying and contextualizing proofs, or will the machines get good at that as well?
My point is that they will, and that is always going to be useful. Bundles of simplified knowledge (in whatever form) that make research simpler will be useful to share whether humans can understand them or not...
Considering how essential math and science is for the prosperity of mankind (not even speaking about the cultural value) the question of how to reward people working and contributing in these fields effectively and appropriately is of extreme importance. (And I think the current decline in our societies is to no small degree caused also by our utter failure to address that issue.)
It is also fascinating, because I don't think there is any solution within our existing system, at least not any I know of. Theorem ownership is not a good solution (and neither are patents in general). Probably the most achievable (or rather the least unachievable) solution is a kind of communist utopia, where people can dedicate their time to a pursuit of any endeavor they see fit, as resources for a decent life are abundant and excessive power capture impossible. (The other option, somewhat dystopian, and which would not require humanity to change too much in its current mode of conduct, would be a totalitarian or caste-like capture of society by the scientific community.)
Incidentally, if AI proves as powerful as some expect it to become, it could bring about another solution of that issue by making all human science and mathematics obsolete, pushing its true market value to zero.
Almost every country in the world has a patent system for a reason...and they are pretty essential for big pharma to function. Granted there should be better calibration of duration - particularly in software, but rewarding first movers is wise in many market conditions. My point regarding "math as a hash list of theorems" is that Theorems will never lose their value, regardless of how powerful AI becomes; they represent compressed knowledge, and as such it will be more efficient for a more advanced AI to query known theorems than reconstruct each one from scratch - in that gap lies a marginal compute saving; an api service or tool call that someone might charge for. Even AI can benefit from specialists...
I disagree. Firstly, people in AI likely care about math on a personal level. Secondly math is useful. Playing go or chess is basically a party trick. Being useful gives it staying power.
But, I do think you are right that there will be some level of moving on. The spotlight is currently on maths and that won't last. It will move to some other area where there is more impact to be had. So while they might shift gears and put less focus on math, it will always be there as part of the portfolio.
I think this is an interesting and good theory. They've probably eked out the large majority of the PR benefit at this point, so whether they continue in this vein will tell us a lot about their motivations for this work.
To take this to the next step, what happened after deep mind pretty much solved Go is that they started looking for the next set of things that hadn't been done yet. It does strike me as very likely that this will follow that same path.
Interesting path forwards, and probably partly true, but there are some important distinctions:
Go was a specialized application. All the math results come as a side effect of reading the whole internet, and it will keep reading the whole internet. It will keep practicing thinking questions. Actually, math might be one of the best ways to keep them contemplating and measure their contemplation abilities, so math will always stay in the loop.
Also, math might not be useful just for humanity, but also for AI, so the system might actively benefit from new math results itself. (Not sure if any of the recent proofs qualify, but future work might.)
I had the same idea recently. You've solved all the famous conjectures (all formulated by humans because humans found them interesting), what next? I doubt "AI formulated a math conjecture that nobody else cares about and immediately solved it" will produce that much hype. The actually interesting thing is indeed how mathematicians themselves will use these AI models going forward and how that will shape mathematics of the future.
I think there’s a venue where they start focusing on introducing hypotheses where the model currently can’t solve it, or maybe this is already happening?
Being able to present useful novel ideas would likely generate a lot of press, for a while. I don’t know how this would look since I’m useless at math, but Im sure there are plenty of unknown problems with massive implications, that once formulated can be solved.
AlphaGo and AlphaZero weren't generalized models. Math capability will presumably keep improving along with the other general capabilities, even if there wasn't a special RL focus for math itself.
>Merely solving not yet solved problem might not be it anymore.
Never has been.
See: Mochizuki's "proof" of the ABC conjecture [1].
In short, mathematics is an art of storytelling as much as anything else.
Writing a boring story, much less an incomprehensible one is worth exactly nothing, and doesn't matter.
Is it cool that the machine can connect the dots that people put out there in a form that happens to be easily ingestible?
Yeah.
Can the machine answer why give a fuck about a result like that?
Nope. That work has already been put in by people.
The most obvious impact of this BS is that interesting problems with potential to be solved, which were already a scarce resource, will no longer be shared.
It's already become a huge issue without AI being involved, due to the rat race nature of academia.
There's even an industry term for when someone gets a wind of another person's progress on such a problem, and solves it before them - it's called "getting scooped"[2].
It doesn't mean that they got access to the results. It can be as simple as e.g. an experienced mathematician hearing about a problem that a PhD student is working on for their thesis, and scooping it.
Honestly, as a mathematician-turned-software-engineer, I see and hear both sides, and both sides are lying:
* The AI companies are lying that what the LLMs produce is "mathematics". Writing a proof, even a correct proof, is not what mathematics is about. The Fundamental Theorem of Algebra has been "proven" incorrectly four times IIRC, but it was mathematics nonetheless.
Mochizuki's "proof", on the other hand, may be correct, but over a decade later, it's still not really mathematics, because transfer of insight is a fundamental component of it, and insight is a thing that the AI, presently at least, doesn't do, no matter how many proofs it produces.
Proof automation has been a field for a long time, for that matter; hyperscaling it doesn't change the nature of things.
The lie is also that a correct proof is the final point. The Four-Color Theorem[3] was proven in 1976, yet people were still proving it 20 years later, trying to reduce the number of cases to leave to the machine, even as we got it super-duper-verified by theorem-proving software in 2005[4].
The writing was on the wall since computers were invented, so why are mathematicians making Pikachu faces now?
That's where the other lie comes in.
* Mathematicians are lying to everyone else by suggesting that the technology is the problem, or that the issue is with how the technology impacts people, and not with the COMPLETELY, ABSURDLY FUCKED UP ORGANIZATIONAL STRUCTURE OF ACADEMIA, and I can't scream it in bold enough caps lock.
There's a reason websites like "100 reasons to NOT go to grad school"[5] exist, and all who've gone through the masochistic 5+ year journey can attest that actually, the reality is worse.
Closer to the point, there's a reason Grothendieck burned most of his work and fucked off from mathematics in the 90s, and Perelman did the same, in effect, in 2000s[6], while putting a million dollar weight to his statement that MATH SOCIETY IS FUCKED.
To all the mathematicians running in circles screaming AaaaAaaAAAaa, Perelman can now say: told you so.
See, after we discussed what math is about (insight transfer), let's do a peculiar little observation that this is exactly what's rewarded THE LEAST in the field.
"Teaching jobs" are a punishment for those who don't do good enough, and doing good means cranking out proofs in a publish-or-perish race, emitting just enough for others to verify correctness, but not too much lest you don't have enough for the next year's publication quota (or, if you are a mastodon, enough for your grad students/postdocs to work on).
The industry where the incentive structure creates and rewards scooping as a concept turned out to be vulnerable to scooping at scale.
O the humanity!
'No Way to Prevent This,' Says Only Industry Where This Regularly Happens.
So the lie to everyone else is that problem isn't 100% a social one in the mathematics community. Not even mathematics.
The way we do math doesn't have to change, and it won't. We've had theorem provers for decades, remember?
What will, I hope, change - what has to change, as Perelman cried out loud (and paid $1M for people to hear him - without listening, it appears) -
- is the way mathematicians treat each other.
That's to say, what gets rewarded, what gets penalized; the incentive structure, and so on.
In Google-speak: the real problem here is that the perf is fucked up, and what counted as impact before can now be automated, threatening the entire hierarchy of resource allocation (in particular, headcount).
This is not only NOT a tech problem (which won't be solved by changing the behavior of AI companies), it's not a problem with the way we do math or adapting to the progress either.
It's the ROTTEN INCENTIVE STRUCTURE OF ACADEMIA that is showing its cracks, and mathematics is where it's apparent the most at this moment because, as Vladimir Arnold told us, mathematics is a branch of physics in which experiments are cheap[7] - and more pertinently, could be performed by LLMs without human involvement.
Unlike the biotech lab where someone still has to wash the beakers, mathematics doesn't have that moat. Hence the conundrum.
Will the mathematical community adapt and fix its publish-or-perish problem, or will it simply become a cult, like it used to be[8]?
Given that a colleague of mine wrote that satire years before LLM proofs were on anyone's radar, I'm not having much hope.
In example of go where I'm more familiar Google deep mind poured large resources to get a super human performance first, establish superiority and abandon it. The community then built their own tools starting from reproducing their papers.
I think similar thing might happen to math. Nobody outside of math cares too much about Hamiltonian cycles in some bizarre graphs or proving lower bounds on complexity of some problem.
Once those results stop being worthy of mainstream media attention, they will abandon math and the progress will be done by mathemicians guiding the models and the community will likely establish some new rules about what makes a valuable contribution. Merely solving not yet solved problem might not be it anymore.