When the speaker began working in the field, Mathlib contained about 30,000 lines of code covering basic finite-set theorems and some basic undergraduate-level mathematical definitions.

“Mathlib is Lean's mathematics library. So it was born about the same time that I started working in the field. It was thirty thousand lines of code containing a bunch of completely basic theorems about finite sets, uh, and some very basic undergraduate-level mathematical definitions, and that was it.”