Short answer: Carina names the University of Washington, CMU, Stanford and UK universities. She says Mathlib began as a teaching effort by Kevin Buzzard at Imperial College London, and two or three of its early contributors now work with Axiom.
Watch this answer from Episode 22 (starts at 13:05) · Episode 22 notes and transcript
From Episode 22: Let's do the Math!, starting at 13:05.
Jordan Metzner [13:05]: Yeah. Okay. So speaking of lean, now that we have everyone has AI, and obviously it's it's almost like for mathematics kind of the jump of like having a calculator versus not having a calculator. Is lean now being taught in these mathematic, educational programs? And are students like writing their math, theorems in lean now? Or is that still too early and we haven't gotten there yet?
Carina [13:27]: That's a great question. I think a lot of universities are teaching Lean. I know a couple of universities in The States, and I know university of Washington, professor Joe Alper in the math department is teaching students Lean. At CMU, there's a really great Lean community. Professor Jeremy Avigad, professor Sean Volick, and others are teaching students Lean. Stanford has an automated reasoning lab by professor Clark Barrett and other folks, and they have TAs that are grad students teaching students Lean. There are many universities in Europe, in The UK that are teaching students Lean as well. In fact, Lean started I mean, not Lean, but Mathlib, the Math Library started as a teaching effort at Imperial College London by professor Kevin Buzzard. He wanted to teach his students who are enrolled in his introductory level, freshman level proofs class to write better proofs and to train them to think rigorously. So he gave these students who might, be a little bit behind on proof writing the exercise of formalizing everything in lean.
Carina [14:34]: What he found is actually it's not those students as his audience, but the students who already don't need the class that, they are very much advanced grad classes takers. And these students, because they are bored and they have nothing better to do, would love to join the effort of formalizing the undergrad corpus of math in Mathlib. And two or three of them are actually currently working with Axiom. Some of Them are, like, my closest friends over, like, the last five years that I met, like, via, like, MIT Imperial College London exchange program. So really sort of great to have these lean native students, and now, like, they're PhD students, some of them have graduated from PhD. But that was, like, 2019, very early on.
