Best Lean-equipped undergrad programs?

Stream: general

[Jon Bannon]

Hi everyone,

I have a very talented high school senior I've been working with here in upstate NY. He's completed the Natural Number Game and the Complex Number Game. He is interested in pursuing math and computer science in university, and he really seems to enjoy Lean. I've been thinking of suggesting he try to go to Brown or Fordham to potentially work with @Heather Macbeth or @Rob Lewis. It occurred to me that it might be a good idea to ask here for recommendations for "best Lean-friendly undergrad departments". I mean, obviously, there's Kevin's group at Imperial, but I don't know if this student will be able to get to London.

The answer to this is probably obvious...that one needs to look at the list of names on the right rather than departments. I thought I might test that assumption, though, before talking with the student this afternoon.

Thank you, in advance, for your feedback!

[Johan Commelin]

I would imagine that CMU is a good place to consider.

[Jon Bannon]

@Johan Commelin : great! Thank you.

[Anne Baanen]

Not to self-promote too much, but both the CS and mathematics departments at the Vrije Universiteit Amsterdam have some Lean users :)

[Patrick Massot]

I assume that if London is too far then Orsay and Amsterdam are probably too far.

[Jon Bannon]

Maybe true, @Patrick Massot , but I'm going to recommend that the student consider Orsay, Amsterdam and London.

[Patrick Massot]

Since you'll be speaking in an American context, you should probably point out that Orsay is much much cheaper than Imperial College in London.

[Jon Bannon]

@Patrick Massot Noted! I imagine that the student might jump at the chance to have access to Jeremy, though. I'll let you know how it goes when I talk with him today. (I will show him this thread, as well.)

I also will note the success you have with undergrads, Patrick. E.g. Anatole!

[Patrick Massot]

A quick google search suggests Orsay is about 200 times cheaper than Imperial.

[Jeremy Avigad]

CMU does indeed seem to be a very good match for his interests. I'd be happy to talk to him.

[Matthew Ballard]

I wouldn't necessarily say "best" but, for some reason, they keep letting me teach Lean-based courses. 3/4 as it currently stands for this year. (And I kinda regret not using Lean for my crypto course :cry:)

[Kevin Buzzard]

Yeah I suspect that for a US student Imperial will cost something like £37000 per year, so comparable to many US institutions. As well as Matt in South Carolina there's Adam Topaz in UAlberta if you think North America is a more feasible alternative.

[Jon Bannon]

@Kevin Buzzard yes, this is comparable to many US institutions.