Hilbert's idea was that by completely formalizing mathematics on a axiomatic/deductive basis, one can mechanically derive proofs so that you don't run into paradoxes/contradictions.
But then Godel showed such a formal system applied to basic mathematics can never be complete (if consistent) and never prove its own consistency.
The work is in creating the theorem / contradiction from that point, but in the big picture, the approach doesn’t have to come from nowhere.
But the "why and what" must always be explained first even if it is incomplete; since that is the problem we are trying to solve. With logic it is even more important since you can follow a proof from one step to the next but by the time you reach the conclusion you have lost the connecting thread to the starting point (for most general folks) i.e. "you have missed the forest for the trees". This is why many folks feel lost when doing mathematics as mere symbol-pushing.