Zulip Chat Archive

Stream: general

Topic: Research internship opportunities around Lean


view this post on Zulip Ryan Lahfa (Feb 23 2021 at 22:07):

Hello there,

I'm an undergraduate student at ENS Ulm, Paris, in computer science and mathematics and I am looking for a short research internships (< 3 months) for this summer.

I was wondering if some folks here were looking for interns or knew of such opportunities.

I would love to work around Lean, I have experience with mathlib / mathematical formalization but I am also interested in program verification and I have done some (automated) in hardware design using symbiyosys.
I can also definitely get up-to-date on some subjects (before the internship) if that's needed at all.

Thanks in advance and thanks for reading!

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:08):

I would take you on but I suspect it would have to be remote (it's unclear what is happening in London) -- I would happily commit to meeting you once a week online though. It would have to be mathematics though, and preferably not analysis because I don't know any

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:10):

I am already working with about five students and more may appear, my plan world be to just devote one full day to meeting everyone and group discussions etc

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:10):

I plan on doing this through July and August

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 23:11):

Probably on Tuesdays

view this post on Zulip Ryan Lahfa (Feb 23 2021 at 23:27):

Kevin Buzzard said:

I would take you on but I suspect it would have to be remote (it's unclear what is happening in London) -- I would happily commit to meeting you once a week online though. It would have to be mathematics though, and preferably not analysis because I don't know any

I would actually be super interested :)

I'm fine with not doing analysis also!

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 00:02):

Great, don't tell Patrick

view this post on Zulip Patrick Massot (Feb 24 2021 at 15:51):

Ryan, if you want to meet someone during this internship then the safest way is to work with me in Orsay (or even with Riccardo in Paris if he is interested). In usual time I would have advised you to go further away, but everything is different those days. I could easily supervise you (in mathematics of course, not program verification).

view this post on Zulip Riccardo Brasca (Feb 24 2021 at 18:08):

If you want to discuss some Lean I would be happy to do it, but Patrick is for sure more experienced than me for a supervision!

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 19:44):

Some might say that this is a good reason for you Riccardo to work with him, because Ryan is probably a pretty safe bet :-)

The situation in the UK that we know it won't be relatively normal until at least the end of June but we have no guarantee that it will be normal then either, right now we just have hopes.

view this post on Zulip Ryan Lahfa (Mar 08 2021 at 10:43):

After thinking about it, I would be glad to do my internship with @Kevin Buzzard but I would welcome any work with @Patrick Massot or @Riccardo Brasca even in real life, ENS only ask us to do an internship not in Paris region (more specifically, Ile-de-France), so doing it officially with @Kevin Buzzard, even if it does not lead to real life meetings, solve the problem IMHO. But I am really motivated to work on any subject (notably sphere eversion :>), would that be an acceptable proposal?
Can I DM you about the paperwork details @Kevin Buzzard if that's possible?

view this post on Zulip Kevin Buzzard (Mar 08 2021 at 12:49):

No problem.


Last updated: May 10 2021 at 00:31 UTC