The majority of the proofs Euclid produced existed, both as theorem and proof, before his time. Similarly, few recent mathematical advances have started with f

The majority of the proofs Euclid produced existed, both as theorem and proof, before his time. Similarly, few recent mathematical advances have started with formalizations and axioms. Calculus wasn't put on a rigorous basis until Lebesgue's time, hundreds of years after Newton and Leibniz. Category theory needed quite some work before it was formalizable. Differential geometry wasn't that rigorous until the twenties or so. Complex analysis was developed using many, many unnecessary assumptions because the formalities weren't there. I'm not picking-and-choosing math fields here; these are just the ones I'm familiar ones. It turns out, axiomatization and theory-building are two separate jobs rarely performed by the same mathematician. Usually, the theory-building makes the mathematician famous, and the axiomatization does not, but this is in many ways a tragedy. In any case, to the outsider of mathematics, it seems that axioms come first. This is false -- axioms come much later, because the work of axiomatizing isn't worth it before the theory proves itself useful. Axioms come first in a formal way, in the same way classes come first in a formal way. But the interesting thing isn't the class -- it's the instance. And in the same way, the axioms aren't interesting -- it's the resulting theories. I found the analogy very insightful.