05:00… 12 10oklopol: it can be proved you cannot prove a few self-referential things
05:00… 12 10Hydrant: there
05:00… 12 10oklopol: true.
05:00… 12 10Hydrant: not nothing :-)
05:00… 12 10vixey: A formal, machine checkable sequence of derivations in some logic which lead to a conclusion
05:00… 12 10oklopol: yes, that basically *doesn't limit us at all*
05:01… 12 10oklopol: a human cannot do that either, we're no better than a computer program at proving stuff, in a theoretical sense
05:01… 12 10vixey: you define your logic and query the computer, which prints out a proof (or goes into an infinite loop or says "no.")
05:01… 12 10vixey: humans are much much better at proving than computers
05:01… 12 10vixey: well,
05:01… 12 10oklopol: the problem with uncomputability is people take the trivial halting problem proof as a proof that there is no use even trying to do automatic proofs etcx
05:01… 12 10vixey: proving interesting theorems
05:02… 12 10oklopol: *etc
05:02… 12 10vixey: a computer can prove 4554454656456454564*54466464868446884486=988977978978978978878787 a lot faster than a human
05:02… 12 10oklopol: vixey: yeah, but no one says that's not just a matter of time
05:02… 12 10vixey: but a human can prove fundamental theorem of ______, whereas a computer wont find it
05:03… 12 10vixey: time and space
05:03… 12 10oklopol: space too?
05:03… 12 10vixey: unless you have unbounded memory you may never find solutions
05:03… 12 10oklopol: neither will humans
05:03… 12 10oklopol: stuff like that makes no sense to even say
05:03… 12 10oklopol: really
05:03… 12 10oklopol: a computer uses space and time more efficiently, we should be using that to say *humans cannot ever find ____*
05:04… 12 10oklopol: just like a human can buy more paper, a computer will probably be able to make use of the universe around it once it can move around
05:04… 12 10oklopol: and find new space to store its intermediary results
05:05… 12 10oklopol: the only real problem is we just don't know anything about anything yet, when it comes to mind, and AI
05:05… 12 10oklopol: .
05:05… 12 10oklopol: not that i know anything, just spouting random shit so i don't have to do my homework.
05:05… 12 10oklopol: i'll continue