The speaker says Mathlib’s maintainers still require contributions to be conceptually well-founded and the right way of doing the mathematics.

“You know, one, one can now question this fundamental design principle that, you know, do we, do we have to find the right level of generality? The Mathlib maintainers, you know, this, this fundamental maths library which everything is building on, we are still absolutely of the, the opinion that to get into our library, it needs to be, it needs to be, you know, conceptually, uh, the right, the right way of doing things.”