Is mathematics one big tautology?

Disclaimer: different people view this differently. I side with Lakatos: Logic is a tool. Proofs are a way to verify one's intuition (and in many cases to improve one's intuition) and it is a tool to check the consistency of theories in a process of refining the axioms. The fact that every proof boils down to a tautology is true but irrelevant to mathematics.

Here is an isomorphic question to the question you posed: A painting is just blobs of paint of different colour on canvas. So, are we to deduce from this fact that the art of painting is reduced to just placing paint on canvas? Technically, the answer is yes. But the painter does much more than that. In fact, it is clear that while the painter must possess quite a large amount of skill in placing paint on canvas, this skill is the least relevant (while absolutely necessary) for the creative process of painting.

So it is with mathematics. Being able to prove is essential, but is the least relevant skill for doing mathematics. In mathematics we don't deduce things from axioms. Rather we try to capture a certain idea by introducing axioms, check which theorems follow from the axioms and compare these results against the idea we are trying to capture. If the results agree we are happy. If the results disagree, we change the axioms. The ideas we try to capture transcend the deductive system. The deductive system is there to help us find consequences from the axioms, but it does not tell us how to gauge the validity of results against the idea we try to capture, nor how to adjust the axioms.

This is my personal point of view of what mathematics is (or at least what a sizable portion of it is). It is very close to what physics is. Physics is not just some theories about matter and its interactions with stuff. Rather it is trying to model reality. So does mathematics, it's just not entirely clear which reality it is trying to model.

It doesn't matter whether every provable theorem is, logically, a tautology. That's just a slightly provocative restatement of the definition of provable.

What matters is via which means such proofs are found. This is where the novel ideas are introduced - in, for example, an ingenious construction, or some clever definition. Or often by going off seemingly on a tangent, proving a few lemmata which at first glance seems to have nothing to do with the theorem in question, only to turn around later, combing the lemmata, and voila, there the theorem.

Note that you can, in some formal systems, actually remove such detours from proofs. That property is called cutfree-ness, and basically states that every proof can be brought into a form where it doesn't take any detours and doesn't proof anything that isn't strictly necessary (that's a very rough description, I know). For such systems, you could argue that it's indeed hard to find creative value in a proof, if the same fact can also be proved in a straight-forward (and boring) way. Luckily for us, it turns out that the property of being cut-free itself has to be something that is very hard to proof. One can show that being cut-free automatically makes a deduction system consistent. Thus, from Gödels theorem, it follows that actually proving cutfree-ness of something like PA has to use methods which themselves go beyond PA's capabilities. Which of course makes cutfree-ness not applicable to the proof of cutfree-ness itself, and this thus always leaves some room for creativity. On just has to pick a strong enough formal system.

Your statement that "Mathematics is a deductive system: it works by starting with arbitrary axioms, and deriving therefrom "new" properties through the process of deduction" is one that many mathematicians (though I presume not all) would disagree with; I am one of them. There is a famous "chairs, tables, and beer-mugs" remark attributed to Hilbert that encourages this point-of-view, but my own view is that the very formal attitude to mathematics that this remark suggests is reflective more of a particular period in mathematics (one when foundational issues were at the forefront, for various reasons) than of the essence of mathematics.

I share the veiw of Ittay Weiss, namely that the ideas come first, and the axioms are just a way to model them. Reasoning, too, often proceeds by working with the ideas first; as the argument develops, eventually it will be molded into something more formal, but (in my experience) this is not how arguments begin their lives.