> 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

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