These two are roughly the same thing. Formally, a proof is just a computation within an axiomatic system. A computation is just transforming one expression into another according to a set of rules. Whether this transformed expression is an algebraic or a logical formula is not a huge difference.
In terms that may be more familiar to programmers, lisp's homoiconicity of data and code corresponds roughly to how Gödel was able to express logical formulae as arithmetic statements via Gödel numbering. Once you are able to encode logical formulae as natural numbers, you can then use laws of arithmetic (e.g. Peano's axioms) to compute/prove other statements/numbers.
