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. 
 A: 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.
