It looks like Qea does verify the proof and generates human-readable text. In that case, my trust in it or Coq would be based on their relative size adjusted for amount of testing these tools received. Coq uses a non-trivially unique proof system (calclulus of coinductive constructions, if I remember correctly), which counts against it. Did anything look what proof system Qea uses?
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.
It seems easier to me to simply trust Coq than to read through 23 megabytes of proofs by eye. But I’m not entirely certain what the purpose of qea is.
It looks like Qea does verify the proof and generates human-readable text. In that case, my trust in it or Coq would be based on their relative size adjusted for amount of testing these tools received. Coq uses a non-trivially unique proof system (calclulus of coinductive constructions, if I remember correctly), which counts against it. Did anything look what proof system Qea uses?
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.