←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 8 comments | 17 Nov 24 17:20 UTC | HN request time: 0.001s | source | bottom
Show context
wslh ◴[17 Nov 24 18:35 UTC] No.42165921[source]▶
If you were to bet on solving problems like "P versus NP" using these technologies combined with human augmentation (or vice versa), what would be the provable time horizon for achieving such a solution? I think we should assume that the solution is also expressible in the current language of math/logic.
replies(3): >>42166040 #>>42166122 #>>42166182 #
1. hiddencost ◴[17 Nov 24 18:50 UTC] No.42166040[source]▶
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.

replies(1): >>42167047 #
2. nybsjytm ◴[17 Nov 24 20:43 UTC] No.42167047[source]▶
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.
replies(2): >>42169055 #>>42169864 #
3. titanomachy ◴[18 Nov 24 01:55 UTC] No.42169055[source]▶
I’m sure AI can “solve” the Riemann hypothesis already, since a human proved it and the proof is probably in its training data.
replies(1): >>42169112 #
4. nybsjytm ◴[18 Nov 24 02:10 UTC] No.42169112{3}[source]▶
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.

replies(1): >>42169872 #
5. Davidzheng ◴[18 Nov 24 05:07 UTC] No.42169864[source]▶
link to this prediction? The famous old prediction of Szegedy was IMO gold by 2026 and that one is basically confirmed right? I think 2027/2028 personally is a breakeven bet for superhuman mathematician.
replies(1): >>42170359 #
6. Davidzheng ◴[18 Nov 24 05:09 UTC] No.42169872{4}[source]▶
what does this even mean? Surely an existing AI could reguritate all of Perelman's arxiv papers if we trained them to do that. Are you trying to make a case that the AI doesn't understand the proof it's giving? Because then I think there's no clear goal-line.
replies(1): >>42169965 #
7. nybsjytm ◴[18 Nov 24 05:33 UTC] No.42169965{5}[source]▶
You don't even need AI to regurgitate Perelman's papers, you can do that in three lines of python.

What I meant is that there's no AI you can ask to explain the details of Perelman's proof. For example, if there's a lemma or a delicate point in a proof that you don't understand, you can't ask an AI to clarify it.

8. nybsjytm ◴[18 Nov 24 06:54 UTC] No.42170359{3}[source]▶
I consider it unconfirmed until it happens! No idea where I saw it but it was probably on twitter.