Could you clarify what point I'm missing? It's true that I am, intentionally, conflating automation and formalisation of mathematics, activities which can be meaningfully distinguished. Is it to that that you object?
On the other hand, I think that it is also meaningful to point out that, although automation is just a version of human activity carried out by a computer, not all human activity is subject to automation—at least, not yet. The two bad examples that spring to mind are chess-playing and facial recognition (bad because both have recently come into the reach of computers).
In principle, any human activity that we understand can be automated simply by giving a computer sufficiently precise instructions; but (1) if those instructions are too detailed and ad hoc, then it may be just as hard to give them as to carry out the task, and (2) there are many human activities that we do not understand.
