New Scientist article about mathematics and computing

A recent article in New Scientist

http://www.newscientist.com/article/mg20126971.800-rise-of-the-robogeeks.html

describes, in the typical vague and sensationalist terms characteristic of so-called popular science journalism, some work of computer scientists Aaron Sloman and Alison Pease, respectively.
After the initial spectacular suggestion that artificial mathematicians may become a reality, the article eventually admits that the actual aim of the research presented is much more modest:

"at this stage he [Sloman] is simply trying to show a link between spatial manipulations and the basics of mathematics."

One should be very careful in extrapolating this into believing fantastic stories about "robot mathematicians". It is also important to remember that the idea of mathematical machines that could prove theorems more or less independently of human input, is not a new one. What can be done today to some extent, is automatic proof check. Several mathematicians have constructed programs that can formally check the validity of certain non-trivial theorems in mathematics, that is, the program finds a deduction from the axioms to the full theorem, using only formal rules of logic. It is quite possible that similar methods could be used to find previously unknown proofs of mathematical results or conjectures, or to handle routine arguments that mathematicians today have to do by hand.
However, mathematics does not simply consist of formal truths deducted from logic, just as a painting does not simply consist of spots of paint on a canvas. Many formal truths are not relevant, and human mathematicians can easily exclude those, but it is very hard to imagine a computer program which would recognize this unformalized (unformalizable?) difference. For instance, a computer might come up with the theorem 2 + 2 = 4, which is relevant, but it could just as well come up with the equivalent theorem "the even prime number plus itself equals the smallest positive even integer square", which is not a mathematically relevant theorem. How is the computer to know which one to choose? It seems it would need human input.
It seems unlikely that a computer, which necessarily works with a formal system as a model of mathematics, will, from some rudimentary axioms alone, come up with such creative products of the human mind as integrals, the category of groups, or etale cohomology, concepts of central importance in modern mathematics. This is because although the proving of theorems seems to be formalizable, the formation of good mathematical definitions, that is, fruitful and enlightening concepts, is something that seems to require human judgement.

The black-and-white statement by Pease that mathematics is not discovered but created is just an empty slogan unless one provides some good argument for it. It is also something that many professional mathematicians would object to. (Indeed, comments at the New Scientist website by readers of the article react against precisely this statement).
It is striking that an article in New Scientist about the possibility of artificial mathematicians, do not feature any statement by an actual mathematician. If you want the best possible opinion about your health, you ask a medically trained person. If you want the most accurate description of history, you ask a historian. If you want the best insight into mathematics you ask a...computer scientist or cognitive psychologist? This reminds me of a quotation by A. N. Whitehead:

"Philosophers, when they have possessed a thorough knowledge of mathematics, have been among those who have enriched the science with some of its best ideas. On the other hand, it must be said that, with hardly an exception, all remarks on mathematics made by those philosophers who have possessed but a slight or hasty and late-acquired knowledge of it, are entirely worthless, being either trivial or wrong."