Summer Internships ETH Zurich

Stream: general

[Tobias Grosser]

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.

[Tobias Grosser]

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.

[Chris Hughes]

(deleted)

[Kevin Buzzard]

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

[Patrick Massot]

Tobias?

[Kevin Buzzard]

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".

[Tobias Grosser]

@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, ...

[Tobias Grosser]

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.

[Tobias Grosser]

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

[Tobias Grosser]

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.

[Tobias Grosser]

@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.

[Tobias Grosser]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

@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.

[Tobias Grosser]

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

[Kevin Buzzard]

I told them that :-)

[Tobias Grosser]

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.

[Tobias Grosser]

Thanks for reaching out.