# algorithmic checking of proofs

Is it possible to check if a proof is correct algorithmically(especially with computer aid)?

I ask this question because I find that a lot of time is taken up during lectures going through the proof of the theorems, which is basically just checking someone else's work(IMO). I think time is better spent if the ideas behind the proof are discussed (how to develop such a method to solve such a problem). Also, I find a proof without motivation very hard to follow.

-
To check a proof "algorithmically" (by computer) you need a formal proof that can be checked line-by-line. This requires being able to algorithmically determine if something is an axiom (among other things); formal proofs are much longer and more laborious to write than regular/informal proofs. But see en.wikipedia.org/wiki/Proof_verification –  Arturo Magidin Apr 8 '11 at 20:09
Related and possible dupe: Complexity of Verifying Proofs –  Aryabhata Apr 8 '11 at 20:18
It's true that sometimes some parts of the proof are "believable" but tedious to verify. However, I doubt that the proofs you are talking about have this problem. At your current stage, it's important to be able to understand proofs so that you can make up ones of your own. A good proof will be accompanied by the relevant intuition, and the challenge is to be able to translate your intuition into a proof. –  Yuval Filmus Apr 8 '11 at 21:07
I have often written a proof thinking "this is clear", then I hear back from someone, saying that "this is not complete, this is wrong, etc" How (if ever) does one know if his/her proof is complete? –  picakhu Apr 8 '11 at 22:54
Being able to give reliable proofs is a skill. Like many skills (i) it is not realistic to expect to attain perfection in it, (ii) one can develop it through practice, especially practice guided by someone who has a high level of that skill and (iii) getting others to do the skill rather than practicing it yourself is thoroughly unhelpful in the long run. –  Pete L. Clark Apr 11 '11 at 6:21

Sure, there's a whole literature on automated deduction, which includes checking proofs as well as finding them.

Automated proof checking is a different thing from what you see in class. Math is all about skepticism and believing things until you have been shown something definitively. Part of that has to do with motivations and concepts, but it wouldn't be math (it'd be philosophy), if you weren't manipulating ideas with some amount of formalism.

What I mean by skepticism is things like making a statement: $$\sum_{n\ge1} 2^{-n} = 1$$ and the mathematical adversary (at a certain level) will say

How do you know that?

You can talk all day about why you care (motivation) or a half minute visualization ("Oh I see now"), but you don't know it until you do some symbolic manipulation (or well-founded conceptual manipulation like the Greeks (ah...this is modern mathematics, not Babylonian or medieval mathematics where you got perfectly fine results without worrying about proof). So the way you know something in math is by, at some point, having to do the detailed grunt work of pushing the symbols around. At a later point you don't have to worry about the pushing around because you know you can do it if you have to. Look at any math journal - it's mostly narratives interspersed with single equations, very few derivations as such or at least they don't look like the mess you see in class (also in class the teacher is probably speaking the narrative, but writing the symbols and leaving out the pictures because they're too hard to draw)/

There's another difficulty and that's pragmatic. In the teaching setting, there are students having all different learning strategies: some are visual, some need repetition, etc, etc and since everything is geared towards merit, it encourages teaching of testable things. And what's more easily testable (in math at least) is derivations (calculations or proofs), not essays on how category theory and set theory are comagisterial foundations of mathematics.

I think I may have gone astray here...yes, it'd be nice to have a little more explanation and motivation of how to get from A to B, but sometimes (most of the time) you also need to show the actual path of A to B.

-
Actually, even before you ask, "How do you know that?" you have to ask, "What do you mean by that." In the case of infinite sums, there's quite a lot of defining to do... –  Thomas Andrews Apr 8 '11 at 22:23