3 ms·

> Correction: Purported formal proofs often actually aren't formal proofs. It is not a proof if it is wrong. Yes, in the strictest sense an incorrect proof is

> Correction: Purported formal proofs often actually aren't formal proofs. It is not a proof if it is wrong. Yes, in the strictest sense an incorrect proof is not a proof. But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. You cannot be unaware of this point. You must have understood what was being conveyed. Yet, instead you decided to engage in a nitpick over the meaning of the phrase "formal proof" Furthermore, your claim that "If you actually come up with a proof, you are completely guaranteed that the proven statement is true." is utterly unhelpful. You know that my point was that a manually verified proof might still be wrong. And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof. So at this point, you are not discussing the questions in good faith, and I'm done with this conversation. (And no, I'm not backing off my position.)

catnaroek 9y ago
> But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. They are wrong. A purported proof is only a proof if it is actually correct. If you cannot reliably come up with a proof, not mere purported proofs, then just be honest and say so. We are not in a consultant-client relationship, so you gain nothing by lying about your skills to me. > You know that my point was that a manually verified proof might still be wrong. Only if you cannot reliably come up with correct proofs. > And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof. It is not an “ill-considered nitpick”. It is essential to my point. If you can prove that your assertions hold, you do not need to check them dynamically. (Of course, this is logically a triviality, and it is awful that I need to explicitly make this point.)

catnaroek 9y ago

> But at the same time, people often call either flawed proofs or purported proofs formal proofs in a looser sense. They are wrong. A purported proof is only a proof if it is actually correct. If you cannot reliably come up with a proof, not mere purported proofs, then just be honest and say so. We are not in a consultant-client relationship, so you gain nothing by lying about your skills to me. > You know that my point was that a manually verified proof might still be wrong. Only if you cannot reliably come up with correct proofs. > And yet rather than addressing that point you decide to evade it by an ill-considered nit pick on whether an incorrect proof is still a proof. It is not an “ill-considered nitpick”. It is essential to my point. If you can prove that your assertions hold, you do not need to check them dynamically. (Of course, this is logically a triviality, and it is awful that I need to explicitly make this point.)