←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
249 points rishicomplex | 2 comments | 17 Nov 24 17:20 UTC | HN request time: 0s | source
Show context
Robotenomics ◴[17 Nov 24 19:30 UTC] No.42166395[source]▶
“Only 5/509 participants solved P6”
replies(1): >>42166999 #
nybsjytm ◴[17 Nov 24 20:36 UTC] No.42166999[source]▶
This has to come with an asterisk, which is that participants had approximately 90 minutes to work on each problem while AlphaProof computed for three days for each of the ones it solved. Looking at this problem specifically, I think that many participants could have solved P6 without the time limit.

(I think you should be very skeptical of anyone who hypes AlphaProof without mentioning this - which is not to suggest that there's nothing there to hype)

replies(2): >>42167113 #>>42168802 #
auggierose ◴[17 Nov 24 20:50 UTC] No.42167113[source]▶
Certainly an interesting information that AlphaProof needed three days. But does it matter for evaluating the importance of this result? No.
replies(2): >>42167292 #>>42168126 #
1. andrepd ◴[17 Nov 24 22:58 UTC] No.42168126[source]▶
More or less. Modern theorem provers, even fully automatic ones, can prove incredibly difficult problems if given enough time. With 3 days and terabytes of memory, perhaps they could? Would be interesting to compare Alphaproof with a standard theorem prover that is given similarly astronomical computing resources.
replies(1): >>42168238 #
2. auggierose ◴[17 Nov 24 23:18 UTC] No.42168238[source]▶
That is an interesting thought. But I doubt that standard automated theorem proving techniques would have solved this in a 100 years, even with immense resources, as all they do is (basically) brute force search, and it remains an exponential search space. Therefore 3 days does not really matter, indeed, 3 months would still be a result that 10 years ago I would have thought impossible.