Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
Yes, because if AI can do maths then it can use that to improve the efficiency/quality of it's algorithms to self improve...
AlphaProof's Greatest Hits
61–70 of 140 posts
Re: AlphaProof's Greatest Hits
#62Earlier quoted context omitted.
No one is focused on those. They're much more focused on more rote problems. You might find them used to accelerate research math by helping them with lemmas and checking for errors, and formalizing proofs. That seems realistic in the next couple of years.
There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of prognostication is definitely out there.
I’m sure AI can “solve” the Riemann hypothesis already, since a human proved it and the proof is probably in its training data.
Re: AlphaProof's Greatest Hits
#63I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
I am building Memelang (memelang.net) to help with this as well. I'd love your thoughts if you have a moment!
Re: AlphaProof's Greatest Hits
#64Earlier quoted context omitted.
There are some AI guys like Christian Szegedy who predict that AI will be a "superhuman mathematician," solving problems like the Riemann hypothesis, by the end of 2026. I don't take it very seriously, but that kind of prognostication is definitely out there.
I’m sure AI can “solve” the Riemann hypothesis already, since a human proved it and the proof is probably in its training data.
No, nobody has proved it.
Side point, there is no existing AI which can prove - for example - the Poincaré conjecture, even though that has already been proved. The details of the proof are far too dense for any present chatbot like ChatGPT to handle, and nothing like AlphaProof is able either since the scope of the proof is well out of the reach of Lean or any other formal theorem proving environment.
Re: AlphaProof's Greatest Hits
#65Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
Yes, because if AI can do maths then it can use that to improve the efficiency/quality of it's algorithms to self improve...
The quality of AI algorithms is not based on formal mathematics at all. (For example, I'm unaware of even one theorem relevant to going from GPT-1 to GPT-4.) Possibly in the future it'll be otherwise though.
Re: AlphaProof's Greatest Hits
#66Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
I doubt it. Math has the property that you have a way to 100% verify that what you're doing is correct with little cost (as it is done with Lean). Most problems don't have anything close to that.
Math doesn't have a property that you can verify everything you're doing is correct with little cost. Humans simply tend to prefer theorems and proofs that are simpler.
Re: AlphaProof's Greatest Hits
#67Anyone else feel like mathematics is sort of the endgame? I.e., once ML can do it better than humans, that’s basically it?
Not the endgame by far. Maybe the endgame for LLMs, and I am not even convinced.
Maths is detached from reality. An AI capable of doing math better than humans may not be able do drive a car, as driving a car requires a good understanding of the world, it has to recognize object and understand their behavior, for example, understanding that a tree won't move but a person might, but it will move slower than another car. It has to understand the physics of the car: inertia, grip, control,... It may even have to understand human psychology and make ethical choices.
Fully autonomous robots would be the endgame.
Re: AlphaProof's Greatest Hits
#68I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
If this were the case, I don't see why we'd need to wait for an AI company to make a breakthrough in math research. The key issue instead is how to encode 'real-life' statements in a formal language - which to me seems like a ludicrous problem, just complete magical thinking.
For example, how might an arbitrary statement like "Scholars believe that professional competence of a teacher is a prerequisite for improving the quality of the educational process in preschools" be put in a lean-like language? What about "The theoretical basis of the October Revolution lay in a development of Marxism, but this development occurred through three successive rounds of theoretical debate"?
Or have I totally misunderstood what people mean when they say that developments in automatic theorem proving will solve LLM's hallucination problem?
Re: AlphaProof's Greatest Hits
#69I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
[dead]
Re: AlphaProof's Greatest Hits
#70I think the interface of LLM with formalized languages is really the future. Because here you can formally verify every statement and deal with hallucinations.
So, you looking for Cyc [1], practically.