Comment by gosub100

Theorem proving is something I'm curious about. Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? I'm not saying its impossible, but why can't you start from 0 = 0, and apply random permutations with symbols on either side, check them for truth, discard the junk, and eventually arrive at the quadratic formula? Or a step further, derive (by randomly applying logical rules) the infinitely-many-primes theorem? Essentially, why can't you just trade CPU cycles for logical proofs and equations? What reading can you recommend that bridges (or addresses) programming language theory (BNF grammars, etc) to mathematics?