[kevinbuzzard]

Just to add my usual disclaimer: the mathlib project is a big open source project and I'm not its leader or even a maintainer of the code base. I am a contributor (as are hundreds of other people) and I talk about it a lot because I think it has the potential to change mathematics. But it is coordinated by many people, like many open source projects.

[deterministic]

Thanks for doing the interview Kevin. I have learned a lot from your articles and interviews over the years. Especially how different the math I care about (computation) is from the math that mathematicians care about (structure).

It is great to see that with Lean/mathlib computer scientists and mathematicians have found a way to work together and benefit from the insights and skills of each other.

So please continue doing what you are doing. I believe it will long term have a massive positive impact on both computer science and mathematics.