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.
