> Efficiency is not important at all when you talk about a mathematical proof. Do we really care about a proof using induction taking n or n^2 operations?

Efficiency and tractability of representation is also an issue, though, and mathematicians (and programmers) do care about that, a great deal. That's why the lambda calculus has been used as the basis for proof assistants such as Coq, whereas Turing machines have not.