At the lowest level, can mathematical proofs be reduced to substitutions and rewrites?

Question

This is the impression I got from reading Douglas Hofstadter's book, Godel, Escher, Bach. He spoke of being able to design a proof checker that applied axioms and theorems to determine if a statement followed from the previous ones. It reminded me of using BNF to check the syntax of statements in a programming language.

Answer 1

Have you seen metamath? It is a formalization of a large amount of mathematics in an extremely simple system:

Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically.

The deduction rules are so simple that they can be (and are) checked by computer.