The really interesting aspect of this, IMHO, is discovering what theorem formulations combine together well as a whole. It's much akin to a software architecture problem.

Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.

One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.

> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.

Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).