8 ms·
Any computable problem will eventually fall to computers. LLMs have made math proofs more computable, in the sense that a computer can both generate potential
by plaidfuji 1mo ago
Any computable problem will eventually fall to computers.
LLMs have made math proofs more computable, in the sense that a computer can both generate potential solutions and check the validity of its solutions on its own, with a reasonable chance of converging on something correct. I assume this was already doable to some extent, but it seems like it’s now exponentially easier. That still doesn’t mean that all math is automatically solved.
This is somewhat similar to things like molecular dynamics or protein folding or finite element simulations, etc. Some problems that were previously intractable via computation became tractable. Others - the vast majority of other problems - remain unsolvable by these computational techniques, because the scale of compute required is beyond imagination. These are simple things like simulating the dynamics of a cubic millimeter of water molecules for 1 second. Unfathomably beyond current capabilities (and LLMs aren’t going to change that).
I think LLMs are great, I use them every day and I think they have a ton of value. But if these things were as revolutionary as people promote/fear them to be, you should immediately point them at the highest value math problems and see progress. Like the Millenium Prize problems. Haven’t seen a solution to those.
So there are limits - but we’re about to learn a lot about the new normal of what constitutes a layup math proof vs the truly difficult.
- gerdesj 1mo ago"Any computable problem will eventually fall to computers." By definition. Its those pesky NP jobbies that get in the way.
- gerdesj 1mo agoJust to re-iterate the point: Whenever the handwaving starts around a discussion relating to a NP hard problem, I find it useful to imagine a Canadian bloke (MHRIP) in a red top, with a ... Scottish accent ... saying: "Ye cannae break the laws o' physics, Jim". (maffs not fisics, obvs!) If that is a bit tiresome for the gung-ho AI evangelist, there is also the rather knotty snag that that blasted Austrian geezer Gödel fiddled up: incompleteness. Its almost as though these bloody clever scientific and that types keep on putting artificial blocks in the way of LLMs laying golden eggs! I'm quite happy with the "marginal gains" I get with a DGX Spark. It will pay for itself within three months doing stuff on prem and us not sending data to someone else. It will scale.
- aorloff 1mo agoScience is not merely computing though, even the theoretical sciences
- VladVladikoff 1mo agoWould be great to see them solve Yang-Mills and Mass Gap.
- GPerson 1mo agoIn my opinion, after seein the Jacobian conjecture go, the Riemann hypothesis only has about a year left. I’m not sure if people just aren’t as aware, but the Jacobian conjecture practically was on par with those other great problems.
- vlovich123 1mo agoWhether or not it’s on par famously or difficulty level doesn’t predict whether the others will fall. They’re unique problems and math isn’t linear - the Jacobian it managed to find a counterexample and relied on other proofs that had been developed showing >3 case == 3 dimensional case. However, the Riemann may not fall in the same way because it may actually be true or the surrounding math isn’t quite ready to tackle that problem.
- GPerson 1mo agoWhen I was in grad school we talked about the Jacobian conjecture as something that would never be solved, and not really even worth thinking about since it’s impossible. There’s been a lot more big open problems solved by AI than which reach the front page of news websites like this. Based on all of these problems getting solved fast I’m just saying I’d be surprised if the Riemann hypothesis lasts another year.
- plaidfuji 1mo agoI would be genuinely very impressed - but still not scared - if the Riemann hypothesis were solved. I suspect that we may require “new math” to make progress on that. If a new operator / symbol is required, is that fundamentally not doable by an LLM because it’s outside of current tokenization space?
- zacmps 1mo agoObviously not, there's no need to create a new character for a new operation. You can just define it as @ or or any other symbol you want.
- deleted 1mo ago[deleted]
- qarl2 1mo agoThey don't need to make NP-hard tractable to shake the world order. They just need to be better than humans.
- jstummbillig 1mo ago> Any computable problem will eventually fall to computers. I think the question, that we keep stumbling over, is what problems are computable. > But if these things were as revolutionary as people promote/fear them to be, you should immediately point them at the highest value math problems and see progress. Like the Millenium Prize problems. Haven’t seen a solution to those. Let the goalpost shifting continue. It'll buy us another half year or so.
- miguelnegrao 1mo agoIf by solution you mean a proof and by testing you mean encoding it in lean and compiling it, the space of possible syntactically correct proofs which you can encode probably explodes in a way that is well beyond what any computer could try to brute-force. LLMs don't brute-force proofs, i believe their approach is quite similar to humans. I believe the same is essentially true for counter-examples of the type that have been found latelly, they are not found by search, but by using theory. On the other hand even if the compute allocated by openai is esquivalent to day 10 human mathematicians, the machines can work 24h per day, that is already a lot more productive.