That is interesting - I think the idea that looms over the whole essay is that we have computers that do logic and can fit those logical operations together, we should be able to give a computer some basic axioms and see what theorems it can construct. Et voila!, there it is. Mention of such a project would have fit the essay well.
Well, the problem is that first-order theories have an infinite number of theorems, so while one can prove as many theorems using a computer as one likes, there is still nothing to say whether they are of any interest or not. Most results are trivial, and in order to find the interesting ones we would have to go digging through a heap mainly composed of uninteresting ones.
This presumes, of course, that one can tell interesting from uninteresting by examining result statements. I am not certain that this is in fact the case. Our appreciation of the importance of a result stems from our ability to connect it to others; for example, König's lemma allows us to prove completeness and compactness (amongst many other things). If we simply saw it stated in symbolic form, amongst millions of others, would we recognise its importance?
