[kmill]

Kevin Buzzard did great work to popularize mathlib among mathematicians (that's how I got involved myself), but he didn't found mathlib!

There's a blurb about the history here: https://leanprover-community.github.io/papers/mathlib-paper....

[Ericson2314]

Oh thanks, I didn't realize. Though, reading that paper, I should have known! Obvious in hind-site that at least some math was going on beforehand.