summer internships at Aalto University, Finland

Stream: job postings

[Kalle Kytölä]

Within the internship programme of the Aalto Science Institute, we have a call for two interns of BSc or MSc level to summer projects on formalization of mathematics in Lean (specifically small topics in probability and analysis). These are topics numbered 4201 and 4202 in the list of internship projects.

If you are interested, you can ask me for more details!

Further advertisement:

• The AScI intership program arranges social events, day-trips, help with housing, etc.
• We are organizing an ICM satellite on Probability and Mathematical Physics in Helsinki just before the ICM itself. The summer interns also get to participate and help in the organization.
• There's a direct train from Helsinki to Saint Petersburg, if you plan to spend your summer vacation at the ICM! (...to hear Kevin's talk, of course :wink:)

[Kalle Kytölä]

In the summer of 2023 we will again have formalization internships at Aalto University. The arrangements are mostly similar to the above (except no ICM satellites this year :grinning_face_with_smiling_eyes: --- which probably means less conference organization and more formalization).

The precise formalization topics are to be selected in due time with the interns' interests and preferences taken into account, but probability and analysis are priorities, because I feel like those areas would particularly benefit from an increased number of contributors. (Also the interns would essentially be a part of our mathematical physics group, where most research topics have a probability / analysis / representation theory flavor.)

Link to the official internship programme info:
https://www.aalto.fi/en/open-positions/aalto-science-institute-asci-international-summer-research-programme-2023

Link to FAQ:
https://www.aalto.fi/en/aalto-science-institute-asci/how-to-apply-to-the-asci-international-summer-research-programme

I'll be happy to answer any questions for example on this Zulip!

[Kalle Kytölä]

In the summer of 2024 we will again have a formalization internship at Aalto University. The arrangements are mostly similar to the last two years, described in this same thread.

The precise formalization topics are to be selected in due time with the interns' interests and preferences taken into account, but probability, analysis, and some algebra are priorities, because I feel like those areas would particularly benefit from an increased number of contributors. (Also the interns would essentially be a part of our mathematical physics group, where most research topics have a probability / analysis / representation theory flavor.)

This year we were supposed to do a bit of coordination/collaboration with a CS professor, too, but I unfortunately don't find his summer project on the internship topics list at the moment. If it works out, that should be a bonus: there might be one more intern doing Lean and there might be some cooler metaprogramming components. If not, the default model will be just being a part of the mathematical physics group and working on some math formalization.

Link to the official internship programme info: (4301 is the number of the formalization project)
https://www.aalto.fi/en/aalto-science-institute-asci/asci-international-summer-research-program-2024-project-list

Link to general information about the AScI internship programme:
https://www.aalto.fi/en/aalto-science-institute-asci/aalto-science-institute-international-summer-research-programme

I'll be happy to answer any questions for example on this Zulip!

[Shreyas Srinivas]

Greetings! May I ask who the CS professor is or more specifically what their research interests are?

[Kalle Kytölä]

I should be a bit careful about saying a lot about the CS part before I have more information. I will try to find out about the status, and I can perhaps say something more in private.

The current public information seems to be that no such CS-side formalization project is listed in the AScI summer internships call. On the other hand, the application period opens only on January 2, so there is a chance we will still see an update (at least some projects seem to have been added to the list at different times).

But at least the math formalization internship exists again this year.

[Malcolm Langfield]

Is there a strict requirement that applicants be currently enrolled in a bachelor's or master's? I'm a couple years our of my bachelor's but quite interested!

[Anatole Dedecker]

FWIW, I spent an amazing summer working with Kalle at Aalto, and I would recommend it to everyone with or without experience in Lean. The whole team at Aalto is wonderful, and there’s a lot of interns on campus during the summer so there’s always someone to have a drink with. And last but not least, the salary is quite high (at least by French standards for internships), and there are enough vacations to enjoy Finnish summer, which is great if you’re like me and think that 30°C is too much :big_smile:

[Yaël Dillies]

I would love to apply but 12 weeks is quite long :sad:

[Kevin Buzzard]

Jason Ying also had a great time at Aalto, and I think a lot of what he did there ended up in mathlib

[Luigi Massacci]

@Kalle Kytölä is there some flexibility on the length? (Would 11 weeks for example be ok)

[Anatole Dedecker]

Obviously you'll have to discuss the length with Kalle, but just as a data point I spent only 9 weeks in Finland last summer. Of course it depends on the experience one has in Lean, from what I saw this summer 12 weeks is a good length for beginners to do something meaningful, but there's absolutely no doubt that Yaël wouldn't need that much time :grinning:

[Kalle Kytölä]

Sorry everyone for responding with such a delay! As an excuse, I had a particularly hectic week (with conference organization and a research visitor on top of the more usual things like a large undergraduate course starting on Monday).

[Kalle Kytölä]

@Malcolm Langfield: The most common situation is interns being BSc or MSc students, but I don't think there is any strict rule for this. The actual official answer would be an administrative matter --- could you ask directly about your eligibility via asci-interns@aalto.fi with the specifics of your situation? Less officially, my own goal is to try to offer something meaningful and in some ways research related (carrying out some project independently, participating in research group activities, attending conferences and/or helping organize them, ...) for a short period of time to talented young people who are likely pursuing a research career (I believe the benefits both to the research community and to the interns themselves are the clearest in such a situation). The most common applicants are students, but I can totally see that there could be different individual circumstances, so as long as the official eligibility criteria are satisfied, I will be happy to consider all applicants!

[Kalle Kytölä]

Regarding the length, there can be some flexibility, but there are also some compelling reasons to try to stick to the default (June-August). Among the reasons to stick to the default are: AScI joint activities (including get-to-know-each-other meetings and final poster presentation sessions etc.), collaboration with other interns, and the supervisor's own semester and summer schedules.

I have so far had two interns who had way more experience on formalization than I do: Anatole Dedecker and Jason KY.. In these cases, the supervision aspect was trivialized: I could just give them basically total freedom and trust that meaningful things will come out. In addition they were both superb at teaching both me and the other interns and in fact yet others in the group and at the department about formalization. I was very lucky to have them! (This is not to take away anything from the other amazing interns I have had, but just to emphasize that there are rare but existing cases where the intern has the most experience on formalization and the relevant math and becomes the teacher to others, and the project can be completely unsupervised. The amount of flexibility is very different in such cases.)

I am super happy there are strong people interested in this. The hopefully fair principle I have in any case is to wait until seeing all applications before considering any particularities, including specifics of duration. Anyone can include their preferred and/or possible schedules in the application. These are ultimately a matter of what we agree in interviews and work contract. In most cases I expect to have a preference for interns who are able to work for June-August, but there can be some exceptions (especially with people who already have significant Lean contributions).

[Kalle Kytölä]

(I also know already beforehand that I will most likely only be able to recruit 1 of the applicants, and there will again probably be more strong applicants than that, so I will feel bad. But I try to comfort myself with 1>0.)