### A Mathematical Proof Too Long To Check

Re:prove that the program works (189 comments)

Um, excuse me. If you're going to quote me and change what I said, then indicate your edits. I have done so above, in bold. Not that I can make sense of them.

Sorry, I realized at one point I was editing the quote rather than my own text and thought I fixed it but apparently missed one of my edits and there's no reason it should make sense there. Entirely my fault.

Wha...? That's just plain wrong. I can think up all kinds of invalid proofs of the Pythagorean Theorem. But showing that a proof is invalid does not mean the theorem is incorrect. It just means your proof is.

Double wha...? I never claimed the theory behind the algorithm is incorrect, just that if an algorithm designed to produce correct proofs produces a fautly proof, the algorithm is faulty. If you think up an invalid proof of the Pythagorean Theorem, you're at fault for violating the rules of the system and I don't know why anyone would claim it's a fault of the system itself.

As for the rest, please see my other reply to your first post, relating to specific vs. universal algorithms. The gist is that a specific algorithm can be written to check the validity of this proof, but doing so is functionally equivalent to manual verification, but a universal algorithm to verify all correct proofs is impossible.

I never said that one couldn't produce either an algorithm that generates proofs or one that verifies proofs, but the fact is, since there exist true statements that are unprovable the latter algorithm cannot be universal. It can only check whether the symbols follow its understanding of the rules of manipulation.

I get what you're saying. Since Program A can be written to conform to certain rules, Program B can be written to confirm the output of A conforms to the rules that A was given, so yes the proof can be "verified" that way, but by definition you're still only covering some of the proofs A might generate.

But note that the poster I originally responded to said that the output need not be evaulated, but rather only the generating algorithm. I never even said this was a useless approach, since it will likely converge to a correct result, but it hardly counts as a proof of the result. Checking programming isn't the same as checking output, and checking output isn't the same as proving mathematical validity, though of course it can be the same as proving that what you get is what you expected to get, which may be good enough in many cases but wasn't even what I was originally responding to.

It may be that I'm assigning too much power to the algorithm that generated the proof. While it's impossible to program an algorithm with the axioms of a system and tell it to generate all the valid proofs of the system, and equally impossible to similarly program one to verify all proofs of the system, some smaller tasks (maybe this one) are certainly within the realm of algorithmic possibility. I was thinking of the original poster's comment in a very general context and not just in that of this specific problem.