I don't think it's really the case that all branches of mathematics really have a 'common basis' as much as that they're all equivalent. It's pretty common to map one branch to another, e.g. arithmetic to set theory, but then once that's been done there's no real reason to write proofs in a particular branch in the formalism of another.
> The idea is that mechanising proof and making it more algorithmic will make it more like what the layman thought proof is , but it at the same time raises the question, what is this all for? Ie maths is what mathematicians do. I think it admits to no clearer a definition. So it’d probably make sense for mathematicians to decide, what precisely is the role of proof?
"A New Kind of Science" has some insights about this that I appreciate greatly. Mathematicians don't bother to enumerate everything that's formally ('mechanically') true, even tho there are some interesting truths to be discovered in that fashion. They instead explore the 'tree of truths' based on history, intuition, and even fashion.
Ultimately, even the most mechanical formal systems are, or can be, nebulous and 'philosophically strange'. Consider the axiom of choice as but one example – there are different set theories depending on whether one accepts that axiom as 'reasonable' (or 'true') or not!