> which Mathlib coalesced as a side-effect of it's capability

Eh, Lean was heavily developed based on feedback from mathematicians; it's not a side-effect but more like a "driving force."

Source: one of Lean's co-authors.