Math understanding: intuitions and proofs I think that cogsci can help me to study a problem in philosophy of math. Consider this case (adapted from M. Detlefsen, Brouwerian intuitionism):

Lucy has the kind of understanding of a given math subject S that we typically associate with the master mathematician. John has a superb ability to manipulate the axioms for S according to logical means. 

Problem: is there a significant difference between Lucy's  knowledge of S and John's knowledge of S? Is it true that the second kind of knowledge does not imply the first? Is it true that Lucy understands S to a certain significant degree), John does not understand S to a certain significant degree.

Are there works in cogsci that can help me to study this problem?

I have found a relatively old article (Arbib, A piagetian perspective on mathematical constructions), but nothing else. 

Thanks very much.
I think it is important here to be clear about what John is really capable of doing.  If all he is able to do is manipulate the axioms of S correctly, this actually does not get him very far, for at least two reasons.  (This is also why theorem proving computer programs have significant limitations.)

1) Suppose we give John a specific theorem P of S and ask him to prove P. Can he do it?  Not necessarily.  There is a set of logical steps based on the axioms that proves P, so it seems within John's reach.  But one problem here is that of computational complexity.  If John proceeds by just, in an undirected fashion, trying to derive new facts of S from the axioms in the hope of eventually arriving at P, the number of paths that he can go down will increase exponentially and it may take longer than the lifetime of the universe for him to arrive at the result.  Master mathematicians in the field of S, on the other hand, have sharp intuitions about what is likely to be an effective path to a proof of P.

2) Mathematicians do more than resolving previously specified open problems.  They also try to generate important new problems.  A mathematician who is not very good at formal proofs may nevertheless make a significant contribution by correctly conjecturing a very interesting result (even if someone else needs to prove it).

1) and 2) overlap somewhat; for example, a master mathematician may conjecture a lemma L in S that is extremely useful for proving P.

If John is not able to do 1) and 2), then it's not clear he is really very skilled at S.  If he is, then it seems that maybe he isn't so different from Lucy after all; somewhere he has the right intuitions.  Maybe Lucy is more consciously aware of her intuitions, perhaps leading into a discussion about what it is like to experience those intuitions.  But many of the intuitions of master mathematicians don't come from conscious processing; certain ways of proceeding just feel right to them but they can't necessarily explain why.