Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I bet the real purpose of qea is that it allowed its author to avoid learning to use something else. But I find it interesting that he recognizes the importance of computer verification for something like this, and maybe it indicates that this has been in the works for a while. It doesn’t have to be half-baked to be wrong, though.
Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I think the idea is that for a point this controversial he is well aware that mathematicians may actually object to his trustworthiness (they’ve objected to less questionable things in the past), and want to verify the proof for themselves. I think he may well be right in this. However, I don’t see why he can’t give a full explanation (his current paper isn’t) for humans as well, since this would probably be finished sooner and would probably save a lot of his own time if there is a mistake.
Yeah, I’ve heard about this “notorious difficulty” in verifying proof checkers before, and I don’t understand what it could mean. Humans are way more unverifiable.
I bet the real purpose of qea is that it allowed its author to avoid learning to use something else. But I find it interesting that he recognizes the importance of computer verification for something like this, and maybe it indicates that this has been in the works for a while. It doesn’t have to be half-baked to be wrong, though.
I think the idea is that for a point this controversial he is well aware that mathematicians may actually object to his trustworthiness (they’ve objected to less questionable things in the past), and want to verify the proof for themselves. I think he may well be right in this. However, I don’t see why he can’t give a full explanation (his current paper isn’t) for humans as well, since this would probably be finished sooner and would probably save a lot of his own time if there is a mistake.