[christopherolah]

>theorem proving is mechanical

I have to disagree. As theorems become more complicated, proving them becomes anything but mechanical: one must choose between an infinite variety of approaches, many of which are equally valid.