Post-human mathematics

Re:Post-human mathematics by vikiomega9 on Monday November 23, 2015 @04:15PM (#10617356)

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"?

[ Parent | on HN ]

Re:Post-human mathematics by JadeNB on Monday November 23, 2015 @06:09PM (#10618015)

> 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.

[ Parent | on HN ]

Re:Post-human mathematics by vikiomega9 on Tuesday November 24, 2015 @11:54AM (#10621899)

   > (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.

[ Parent | on HN ]