Research internship opportunities around Lean

Stream: general

[Ryan Lahfa]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I plan on doing this through July and August

[Kevin Buzzard]

Probably on Tuesdays

[Ryan Lahfa]

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!

[Kevin Buzzard]

Great, don't tell Patrick

[Patrick Massot]

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

[Riccardo Brasca]

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!

[Kevin Buzzard]

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.

[Ryan Lahfa]

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?

[Kevin Buzzard]

No problem.