3 ms·
You know this reminds me of A Deepness in the Sky where groups of "focused" humans with the aid of computers had to be guided toward what's "interesting" to kee
by vikiomega9 11y ago
You know this reminds me of A Deepness in the Sky where groups of "focused" humans with the aid of computers had to be guided toward what's "interesting" to keep them from going into loops by other normal humans.
> Can all interesting proofs be built with human-friendly steps?
That is a marvelous question. How would one even quantify "human-friendly"?
- JadeNB 11y ago> How would one even quantify "human-friendly"? Presumably in much the same manner as the Turing test, by showing it to humans (well, human mathematicians) and letting them judge it. In fact, one can imagine a Turing test for ATPs in which they have to produce proofs that will fool a referee. I can't decide whether I think that this would be harder (because who, including they themselves, knows how human mathematicians mentally explore their subject?), or easier (because of the much more specialised domain knowledge), than the full Turing test.
- vikiomega9 11y ago> (because who, including they themselves, knows how human mathematicians mentally explore their subject?), or easier (because of the much more specialised domain knowledge), Indeed, the problem is you have to walk up and down various abstract constructions that define what a human mathematician is.