Is it a contradiction, if
- I am a formalist
- I think that mathematical objects are created by human mind
- In other words: Am I allowed to be a formalist and to believe that mathematical objects are created by human mind?
There is not a contradiction. Formalism is insistence that only the form, and not the content of mathematics is really mathematical. So the content can be motivated by anything from religion to politics to whim. As long as only the result, and not its motivation, really matters to you, the two can coexist.
Most formalists still allow themselves to fall back into Platonism for concreteness, knowing that if they wander too far, they will encounter real, basic paradoxes, but not caring, because the effect of these explorations is what matters, and not their content.
But I feel there are more productive ways to look at this approach to mathematics than to ignore half of your belief. Much good mathematics is motivated by a faith we share about our interpretation of the world. And formalism demands this be put aside entirely, as it lies outside mathematics proper.
I think this psychological/mentalist view of mathematics deserves attention, and that its first genuine form is reflected in Brower's 'intuitionism'.
--- To address the comment ---
I may be 'really doing' physics. The content may be intrinsically tied to matter and masses, etc. But that, then is not a part of the mathematics involved. From a formalist view the fact that it takes a specific form makes it mathematics (they do not agree absolutely on the relevant aspects of that form). So for abstract reasoning, Platonic religion, or aspects of physics, or the psychological confusion caused by word games can equally be motivation.
We can factor out the mathematics from the irrelevant content based upon the form it takes. Despite the statements of the problems they solve, the marriage etable algorithm has nothing to do with romance, and the convergence of the probability of derangments has nothing to do with hats. Euclidean geometry has nothing to do with pictures. Formalism just takes this observation to its logical extreme.
Brower (a geometric topologist) rejects this because it rules out the process of geometry to a huge degree. What geometrically-oriented thinkers, including many real analysts and topologists, and even abstract algebraists who focus on diagrams that capture combinatorial forms or depictions via category theory do, mathematically, is largely an aspect of their perceptual apparatus, which they translate into words or diagrams. But the nature of the idealized shapes themselves seem to be germane, and to be inseparable from the mathematics. The content is forced into relevance in order for any interpretation to retain the intended meaning. (He overcorrects by insisting all mathematics is basically non-linguistic, ignoring modern forms, like model theory and all the algebra it encompasses, which are in intention entirely linguistic. But the point is that we should not throw out Classical math, or any other part, not that we should put rigid boundaries around future math.)
The compromise then is to say we are studying the mechanism of abstraction itself. We are doing applied psychology, while the formalists are doing applied semantics. Abstract semantics, is, of course, part of linguistics which is a close cousin to psychology, so the two camps largely get along. But we feel that formalism lacks 'a soul' that mathematics used to retain via Platonism.
By focussing on the fact this is an exploration of an important aspect of human nature, mathematics gets back a grounded purpose, and the immediacy and passion that it can incite makes some sense. To be genuinely excited by abstract semantics seems anomalous, philosophically. But it is very, very common for real mathematicians to be deeply invested.
I think to answer the question it would be helpful to look at the origins of formalism in the present-day sense. Formalism is a doctrine regarding justification; it is an essentially epistemological position that certainly carries over into methodological concerns and theoretical results. It seeks to answer questions like--under what circumstances can I know that (or be justified in holding that) I can operate freely with infinite sets, imaginary quantities, and so forth, and still trust the result?
The answer, for formalists, is precisely when you can show that you are working within a complete formal system, defined by symbolic axioms in an unambiguous formal language, where any inference is made according to a basic set of logical transformation rules. Since the axiom system would be complete, one would know that it is closed under the transformation rules, and that thereby any concept employed in a theorem, lemma, etc., would have a valid implicit definition via the axioms, regardless of any semantics we want to assign it.
The reason this solves the problem I mentioned in the first paragraph is this: "infinite" sets, "imaginary" quantities--all of these are interpretations of the syntax that is employed in a (formalist conception of) a formal system. The actual mathematical results are at the level of syntax and thus independent of these semantic interpretations. Hence the problems associated with interpreting mathematical results in these ways become mere pseudo-problems, artifacts of mathematics done in the old style, prior to mathematicians obtaining the methods that would allow Hilbert to envision in a very explicit way the possibility for showing that an interesting axiom system could be proven complete (this was of course shown to be impossible in any grand, sweeping sense by Godel's famous impossibility results).
The problem, then, with your question is this: formalism--in itself-- doesn't require there to be any mathematical entities at all. Again, this would be an interpretation of the mathematical results. Hence, they are neither Platonic, nor created by the human mind. A "mathematical object" is only an object to the extent that it can be implicitly defined by the deductive relations it takes on within a given set of axioms.
If you wanted to both be a formalist and hold fast to the idea that mathematical objects are constructs of the human mind, you'd have to answer how and why it is that you are allowed non-constructive proofs. For, within formalism "mathematical objects" are, again, implicitly defined in a syntactic way, and therefore you don't need to actually construct the object to prove its existence; you would only need to show its logical consistency within the system defined by the axioms (hence the well-known dictum that consistency is the criterion of "mathematical existence."). On the other hand, if mathematical objects are constructs of the human mind, most hold that you would have to actually give a method for constructing any alleged object before it was accepted that such an object can actually be worked with. In other words, your philosophical convictions would be dissonant with the kinds of methods that formalists take for granted.