←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 3 comments | 17 Nov 24 17:20 UTC | HN request time: 0.622s | 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 #
nybsjytm ◴[17 Nov 24 21:10 UTC] No.42167292[source]▶
I agree that the result is important regardless. But the tradeoff of computing time/cost with problem complexity is hugely important to think about. Finding a proof in a formal language is trivially solvable in theory since you just have to search through possible proofs until you find one ending with the desired statement. The whole practical question is how much time it takes.

Three days per problem is, by many standards, a 'reasonable' amount of time. However there are still unanswered questions, notably that 'three days' is not really meaningful in and of itself. How parallelized was the computation; what was the hardware capacity? And how optimized is AlphaProof for IMO-type problems (problems which, among other things, all have short solutions using elementary tools)? These are standard kinds of critical questions to ask.

replies(2): >>42167378 #>>42170461 #
dash2 ◴[17 Nov 24 21:19 UTC] No.42167378[source]▶
Though, if you start solving problems that humans can't or haven't solved, then questions of capacity won't matter much. A speedup in the movement of the maths frontier would be worth many power stations.
replies(1): >>42167482 #
nybsjytm ◴[17 Nov 24 21:30 UTC] No.42167482[source]▶
For some time a 'superhuman math AI' could be useful for company advertising and getting the attention of VCs. But eventually it would be pretty clear that innovative math research, with vanishingly few exceptions, isn't very useful for making revenue. (I am a mathematician and this is meant with nothing but respect for math research.)
replies(2): >>42168017 #>>42171919 #
1. airstrike ◴[17 Nov 24 22:39 UTC] No.42168017[source]▶
"Making revenue" is far from being the only metric by which we deem something worthy.
replies(1): >>42168169 #
2. nybsjytm ◴[17 Nov 24 23:07 UTC] No.42168169[source]▶
As a mathematician, of course I agree. But in a sentence like:

> A speedup in the movement of the maths frontier would be worth many power stations

who is it 'worth' it to? And to what end? I can say with some confidence that many (likely most, albeit certainly not all) mathematicians do not want data centers and power stations to guzzle energy and do their math for them. It's largely a vision imposed from without by Silicon Valley and Google research teams. What do they want it for and why is it (at least for now) "worth" it to them?

Personally, I don't believe for a second that they want it for the good of the mathematical community. Of course, a few of their individual researchers might have their own personal and altruistic motivations; however I don't think this is so relevant.

replies(1): >>42170367 #
3. auggierose ◴[18 Nov 24 06:55 UTC] No.42170367[source]▶
There is something called applied math, and there is a big gulf between applied math and pure math. This new technology has the potential of making use of much more "pure math" for applied math, unifying much of pure math, applied math, and programming. I don't really care about the RH, I care about that.