Zulip Chat Archive

Stream: general

Topic: Summer Internships ETH Zurich


view this post on Zulip Tobias Grosser (Nov 24 2018 at 12:44):

Dear students,

we just announced the ETH Summer internship program specifically targetted at BSc and MSc students: https://www.inf.ethz.ch/studies/summer-research-fellowship.html. We feel it is a great way for young students to gain first research experience! While lean is not yet so widespread at ETH, we certainly have people interested. Get in touch with me if this is something you would be excited about.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 12:47):

Dear senior researchers, please pass this on to your students. I feel this would be a great way to get more lean into ETH. With Johannes' presentation we planted a first seed, Sebastian will give another talk soon, having some lean student projects at ETH would be a great way to continue.

view this post on Zulip Chris Hughes (Nov 24 2018 at 12:59):

(deleted)

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 14:47):

Who would supervise someone interested in writing Lean code at ETH?

view this post on Zulip Patrick Massot (Nov 24 2018 at 14:55):

Tobias?

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 14:57):

There seems to be some list of professors at https://www.inf.ethz.ch/studies/summer-research-fellowship/professors.html -- I maybe misread it as "you should choose one of these people".

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:10):

@Kevin Buzzard, that's a good question. I feel there is a chicken and egg problem to get things rolling, especially as I am myself not well trained in lean. Depending on the topic I would collaborate with people proficient in Isabelle (David Cock, Dmitriy Traytel), remote-collaborate with interested parties on Zulip (maybe Rob?), invite senior people on lean for a similar period, ...

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:12):

On the lean side, this is clearly not the best place to work with lean die-hards, but especially for students who are comfortable to work on open source projects with the community and potentially already took a first course in lean, we certainly would have interesting problems to work on. Also, they would help to establish lean as a tool at ETH.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:12):

I talked with several people and there is clearly interest here.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:14):

There seems to be some list of professors at https://www.inf.ethz.ch/studies/summer-research-fellowship/professors.html -- I maybe misread it as "you should choose one of these people".

These are examples of researchers at ETH. I am officially associated to Torsten Hoefler, but in the end students work on concrete projects with any of the senior staff at ETH.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:16):

@Kevin Buzzard, you have a lot of experience working with young students. My feeling is that students who worked with you for a year on lean might be a good fit.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:17):

Any advice or recommendation what would help to make an internship at ETH for them a valueable experience would be very much appreciated.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 15:20):

OK this is great. I was composing an email to the Xena people at Imperial -- this is why I was asking -- I realised I was not sure whether it would be possible to work with you / your group (there seem to be a wide range of interests represented, unsurprisingly, in the program). We have such a program in the UK called UROP -- I had 20 students working with me last summer, formalising parts of the mathematics curriculum at Imperial.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 15:25):

@Tobias Grosser I told the Imperial people. You should maybe advertise it on the lean-user mailing list? It seems like a sensible use of it.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:26):

If people want to work specifically with me, they should reach out to me.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 15:27):

I told them that :-)

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:27):

This specific program is our flagship program to attract young students. It is a great tool to reach out, but we have various other options which we can use depending on our project needs.

view this post on Zulip Tobias Grosser (Nov 24 2018 at 15:27):

Thanks for reaching out.


Last updated: May 18 2021 at 17:44 UTC