I will present the social enterprise behind the 2 million lines-of-code library of formalised mathematics Mathlib, highlighting the ingredients of its success beyond the purely technical prowess.