Zulip Chat Archive

Stream: general

Topic: Best Lean-equipped undergrad programs?


Jon Bannon (Sep 30 2022 at 11:58):

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 (Sep 30 2022 at 12:06):

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

Jon Bannon (Sep 30 2022 at 12:48):

@Johan Commelin : great! Thank you.

Anne Baanen (Sep 30 2022 at 12:50):

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

Patrick Massot (Sep 30 2022 at 12:53):

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

Jon Bannon (Sep 30 2022 at 12:55):

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

Patrick Massot (Sep 30 2022 at 12:57):

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 (Sep 30 2022 at 12:58):

@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 (Sep 30 2022 at 13:02):

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

Jeremy Avigad (Sep 30 2022 at 14:10):

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

Matthew Ballard (Sep 30 2022 at 15:38):

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 (Sep 30 2022 at 18:20):

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 (Sep 30 2022 at 20:27):

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


Last updated: Dec 20 2023 at 11:08 UTC