←back to thread

AlphaProof's Greatest Hits

(rishimehta.xyz)
248 points rishicomplex | 4 comments | 17 Nov 24 17:20 UTC | HN request time: 0.862s | source
Show context
nybsjytm ◴[17 Nov 24 20:34 UTC] No.42166977[source]▶
Why have they still not released a paper aside from a press release? I have to admit I still don't know how auspicious it is that running google hardware for three days apiece was able to find half-page long solutions, given that the promise has always been to solve the Riemann hypothesis with the click of a button. But of course I do recognize that it's a big achievement relative to previous work in automatic theorem proving.
replies(2): >>42167197 #>>42167309 #
whatshisface ◴[17 Nov 24 21:00 UTC] No.42167197[source]▶
I don't know why so few people realize this, but by solving any of the problems their performance is superhuman for most reasonable definitions of human.

Talking about things like solving the Reimman hypothesis in so many years assumes a little too much about the difficulty of problems that we can't even begin to conceive of a solution for. A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get the answer wrong.

replies(3): >>42167281 #>>42167469 #>>42167489 #
1. nybsjytm ◴[17 Nov 24 21:31 UTC] No.42167489[source]▶
> A better question is what can happen when everybody has access to above average reasoning. Our society is structured around avoiding confronting people with difficult questions, except when they are intended to get the answer wrong.

What does this have to do with a hypothetical automatic theorem prover?

replies(1): >>42167681 #
2. whatshisface ◴[17 Nov 24 21:58 UTC] No.42167681[source]▶
Logic is pretty much absent from our culture and daily life, but that could be due to its limited supply.
replies(1): >>42167744 #
3. nybsjytm ◴[17 Nov 24 22:04 UTC] No.42167744[source]▶
Being logical in social life is pretty much completely different from being logical in a mathematical argument, especially in a formal theorem proving environment. (Just try to write any kind of cultural proposition in a formal language!)
replies(1): >>42168090 #
4. whatshisface ◴[17 Nov 24 22:52 UTC] No.42168090{3}[source]▶
That's the way things are now, but this regime came about when proving things took intense concentration and specialized skills that very few people had. Contrast going to look something up in a library with googling something during a conversation.