Comment by kuboble
7 hours ago
It has utility so some people will pursue it, but it has no immediate business value so I don't believe ai labs will keep spending millions on it.
Unless they decide that trying p!=np is worth any money.
7 hours ago
It has utility so some people will pursue it, but it has no immediate business value so I don't believe ai labs will keep spending millions on it.
Unless they decide that trying p!=np is worth any money.
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.
> often these techniques are invented first and the applications come later
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:
https://hn.algolia.com/?q=usefulness+of+useless+knowledge
The deluge of maybe-proofs have the same problem as the Library of Babel.
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.