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?
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.
(With apologies for rambling.)
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.
https://en.chessbase.com/post/the-full-alphazero-paper-is-pu...
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.
https://deepmind.google/blog/alphazero-shedding-new-light-on...
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.
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 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.).
Problem is, that type of research is much harder. Some doubt that progress in such areas will be quick (https://www.noahpinion.blog/p/wheres-the-intelligence-explos...).
You can believe they believe they are telling the truth or that they have good intentions while still being skeptical of the effective trajectory.
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
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.
Unless they decide that trying p!=np is worth any money.
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.
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.
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.
There's a great paper from Abraham Flexner on this topic:
https://worrydream.com/refs/Flexner_1939_-_The_Usefulness_of...
It argues exactly that we should be allowed to pursue the seemingly "useless" knowledge.
Previously discussed on HN:
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.
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.
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.
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 :)
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.
Ah this is an enlightening point. 8 hadn't thought about it this way, but you're right.
Don't hire a straight-A student, unless it's to take exams; or a professor, unless it's to write papers.
-- Nassim Taleb
-- Me
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.)
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.
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.
Stay tuned.
[1] https://www.quantamagazine.org/titans-of-mathematics-clash-o...
[2] https://quantixed.org/2018/03/19/scoop-some-practical-advice...
[3] https://en.wikipedia.org/wiki/Four_color_theorem
[4] https://en.wikipedia.org/wiki/Proof_assistant
[5] https://100rsns.blogspot.com
[6] https://www.nbcnews.com/id/wbna38039068
[7] https://archive-dsweb.siam.org/The-Magazine/All-Issues/vi-ar...
[8] https://www.mcsweeneys.net/articles/an-open-letter-to-the-ma...
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.