←back to thread

249 points rishicomplex | 1 comments | | HN request time: 0.216s | source
Show context
nybsjytm ◴[] 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 ◴[] 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 #
nybsjytm ◴[] 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 #
whatshisface ◴[] 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 #
nybsjytm ◴[] 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 #
1. whatshisface ◴[] No.42168090[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.