> By canonization, I mean the process of taking a local, one-off formalization and turning it into library mathematics: general, reusable, coherent, efficient, and compatible with the rest

I think this kind of work is constantly misunderstood and undervalued. I don't really see it as a binary thing, more like a complex skill that most people are terrible at, some are good at, and a handful of giants use to be just ridiculously productive in their field.

It reminds me of hedgehogs and foxes - foxes tend to be bad at making one off progress on their own, but are critical for accretive work.

Also I was reading a textbook the other day and thinking wow, it is absurd how much more valuable these things can be than other resources, and it's exactly because they canonize. It would be a massive loss if they stop getting written.