## Stream: general

### Topic: summer program for undergrads

#### Jeremy Avigad (Feb 10 2020 at 18:20):

Carnegie Mellon Summer School in Logic and Formal Epistemology:
It's a good deal : free classes and dorm rooms for three weeks, and they have a great time. Please share this with promising young people! We can accept 25 students (we typically get about four times that many applicants).

#### Donald Sebastian Leung (May 06 2020 at 10:37):

Not sure if this is the right topic for The Xena Project summer projects, 2020 but I was just wondering what is the preferred method of application and deadline?

#### Johan Commelin (May 06 2020 at 10:48):

@Kevin Buzzard :up:

#### Kevin Buzzard (May 06 2020 at 11:45):

So apparently announcing this but giving no preferred method for anything because I am not even going to think about stuff until June, is causing some issues :-)

#### Kevin Buzzard (May 06 2020 at 11:46):

@Donald Sebastian Leung you are young. What do you suggest that the preferred method of application should be? People are getting in touch with me saying "OK so what now?" and my answer is "nothing, yet, just learn some Lean"

#### Kevin Buzzard (May 06 2020 at 11:46):

Should I be sending them to Discord or Instagram or something?

#### Alastair Horn (May 06 2020 at 12:58):

I'm looking to join in here and I think it would be great to get in touch with others, I think you should set up a place (discord would work great) where undergrads who want to be part of this can chat about maths and lean and get to know each other?

#### Kevin Buzzard (May 06 2020 at 13:00):

I already have a discord Lean server, but I've not really used it to do any Lean yet: https://discord.gg/AnHKcDm

#### Donald Sebastian Leung (May 06 2020 at 14:51):

Kevin Buzzard said:

Donald Sebastian Leung you are young. What do you suggest that the preferred method of application should be? People are getting in touch with me saying "OK so what now?" and my answer is "nothing, yet, just learn some Lean"

I haven't used Discord myself (I'm kinda old-fashioned for someone my age :stuck_out_tongue: ) but @Alastair Horn 's idea sounds great. Though I think it would still be beneficial to maintain a certain level of formality and require interested applicants to contact you by email to prove their sincerity.

#### Johan Commelin (May 06 2020 at 14:53):

@Kevin Buzzard I've also never used Discord. But why don't you set up a Xena stream here, and tell people to start there?

#### Johan Commelin (May 06 2020 at 14:53):

Then they "close to the fire" so to speak

#### Patrick Massot (May 21 2020 at 11:42):

I'd like to understand more about @Kevin Buzzard summer project. I have precise questions:

• What are the students commitments? What do you expect them to promise to do?
• What are Kevin's commitments? What do you promise to do? In particular, could you clarify that, contrary to your regular UROPs, there is no money involved.
• Is there anything like a selection, or a cap on the number of involved students?
• Should I ask my students whether they are interested in participating?

#### Kevin Buzzard (May 21 2020 at 14:58):

I ran summer projects in 2018 and it was kind of chaos. Some people took money and did nothing. Some people had no money and did lots of things. Some had filled in the UROP form. Some hadn't. I had no formal record of who was involved but a few times a week I would spend the day in Imperial's math department computer room talking to people, listening to their issues and then explaining that they would have to ask Chris

#### Kevin Buzzard (May 21 2020 at 14:58):

Or, if I was lucky, I could sometimes help

#### Kevin Buzzard (May 21 2020 at 14:59):

And then some people made mathlib PRs, some people made standalone projects, and nobody really wrote anything up but we all agreed we'd learnt a lot

#### Kevin Buzzard (May 21 2020 at 14:59):

This year my aims are slightly higher

#### Kevin Buzzard (May 21 2020 at 15:00):

I am not a fan of administration so there is no registration process and no money involved. I will spend tuesdays and Thursdays online at Zulip and Discord answering questions

#### Kevin Buzzard (May 21 2020 at 15:02):

But the advice I will be giving everyone is just to make their own lean project, host it on GitHub, prove a theorem or make a conjecture or a definition but then they have to promise two things: firstly that their code compiles with no errors and with the version of mathlib stated in their toml

#### Kevin Buzzard (May 21 2020 at 15:02):

And second that they attempt to document their code

#### Kevin Buzzard (May 21 2020 at 15:03):

And then we leave the code to rot because if it compiles once, you win

#### Kevin Buzzard (May 21 2020 at 15:03):

I know it's not how you'd do it Patrick

#### Kevin Buzzard (May 21 2020 at 15:04):

But it's all I can manage

#### Patrick Massot (May 21 2020 at 15:04):

Why do you say this is not how I would do it?

#### Kevin Buzzard (May 21 2020 at 15:04):

In particular no cap and sure tell your students

#### Kevin Buzzard (May 21 2020 at 15:04):

Because you would organise something properly

#### Kevin Buzzard (May 21 2020 at 15:05):

Whereas I prefer chaos

#### Patrick Massot (May 21 2020 at 15:05):

Oh I see. But the question is moot anyway. I would never promise to do so much during summer. My kids are too young.

#### Patrick Massot (May 21 2020 at 15:08):

I think it would be nice to put all those answers on your dedicated web page.

#### Yury G. Kudryashov (May 21 2020 at 18:01):

@Kevin Buzzard It would be nice to have a list of these students' repos somewhere in mathlib (either as a github issue or as an .md/.yaml file with links and short descriptions).

#### Patrick Massot (May 21 2020 at 18:03):

And now the twitch streaming has ended, Kevin should update his website.

#### Yury G. Kudryashov (May 21 2020 at 18:04):

Or replace "have a repo with code that compiles" with "have a PR that compiles (no requirement to have it merged)".

#### Kevin Buzzard (May 21 2020 at 19:17):

@Yury G. Kudryashov this is a great idea. I would happily make the yaml file. Can you start it off for me? I've never made one before. I know a bunch of repos which I would loosely associate with "the Xena project". For example this: https://github.com/LAC1213/compact_unit_ball or this https://github.com/ImperialCollegeLondon/xena-UROP-2018/tree/master/src/Geometry

#### Kevin Buzzard (May 21 2020 at 19:19):

@Patrick Massot : the object of the summer program is to add to the forthcoming yaml file which I will populate once I know what a yaml file looks like.

#### Patrick Massot (May 21 2020 at 19:20):

Which yaml file? We have lots of them nowadays

#### Kevin Buzzard (May 21 2020 at 19:21):

Here's a pretty crazy project https://github.com/kckennylau/local-langlands-abelian

#### Kevin Buzzard (May 21 2020 at 19:22):

I just want to know how to turn these random URLs which I am posting here (and there are plenty more things -- stuff which compiled, some of it really interesting

#### Kevin Buzzard (May 21 2020 at 19:23):

An undergraduate made fundamental groups. Do we even have them in mathlib?

No we don't

#### Kevin Buzzard (May 21 2020 at 19:26):

More and more of these projects are appearing. That's the job of the Xena Project -- to get maths students that I know or have met online to formalise interesting stuff. @Bhavik Mehta 's very impressive work on the Kruskal Katona theorem is something which I really encouraged him to work on and helped him to start out with it. I have no idea whether it will end up in mathlib before we are engulfed by Lean 4 but as far as I'm concerned, if it worked once, and if I could kind of see what you had done, then you had passed.

#### Kevin Buzzard (May 21 2020 at 19:26):

Talking of which, Ali Sever passed this week

#### Bhavik Mehta (May 21 2020 at 19:27):

For what it's worth, the proof still works on yesterday's version of mathlib and lean: https://github.com/leanprover-community/mathlib/tree/combinatorics/src

#### Patrick Massot (May 21 2020 at 19:28):

Yesterday?! That's pretty old! It means you're probably still fighting (|

#### Yury G. Kudryashov (May 21 2020 at 19:29):

@Kevin Buzzard Why not open PRs for all of this?

#### Yury G. Kudryashov (May 21 2020 at 19:29):

If the author doesn't want to polish it, then add a please-adopt label right away.
@Bhavik Mehta :up:

#### Alex J. Best (May 21 2020 at 19:29):

Yaml is easy enough, its just data in record, you could lay it out like this:

- link: https://github.com/leanprover-community/mathlib/tree/combinatorics/src
author: Bhavik Mehta
description: >
Kruskal-Katona is great
status: finished
author: Alex
description: >
status: in progress


#### Alex J. Best (May 21 2020 at 19:32):

you could add whatever fields you like, "mathlib-version : 3.14" for instance

#### Bhavik Mehta (May 21 2020 at 19:39):

Yury G. Kudryashov said:

If the author doesn't want to polish it, then add a please-adopt label right away.
Bhavik Mehta :up:

#### Patrick Massot (May 21 2020 at 19:41):

Yury is pretty efficient at threatening people until they PR. We should use that more often

#### Bhavik Mehta (May 21 2020 at 19:42):

I had already made a few PRs from there but I didn't realise there was an option to dump it in someone else's lap

#### Yury G. Kudryashov (May 21 2020 at 19:44):

Possibly no one will pick it up but at least someone who'll decide to formalize the same theorem will see what's already done.

#### Kevin Buzzard (May 21 2020 at 20:51):

Many of my students write code which is not appropriate for mathlib and have no desire to get it into a state which would be appropriate

#### Ryan Lahfa (May 21 2020 at 21:29):

That sounds like something I can pick up and fix it while not thinking too much

#### Patrick Massot (May 21 2020 at 21:30):

This is not the usual situation

#### Patrick Massot (May 21 2020 at 21:30):

You should rather expect to have quite a bit of work

#### Bryan Gin-ge Chen (May 21 2020 at 21:39):

@Ryan Lahfa Awesome, I'm assigning the PR to you, let us know when it's ready for review.

#### Bryan Gin-ge Chen (May 21 2020 at 21:42):

.... or rather, I'll assign it to you once you accept the invitation to collaborate on mathlib.

#### Ryan Lahfa (May 21 2020 at 21:42):

Bryan Gin-ge Chen said:

.... or rather, I'll assign it to you once you accept the invitation to collaborate on mathlib.

accepted

#### Ryan Lahfa (May 21 2020 at 21:44):

Patrick Massot said:

You should rather expect to have quite a bit of work

But it's "repeat {here's a more mathlib-way of doing stuff, are core maintainers okay with it now? — Patrick: no}" until it works?
I'm okay with spending time to do iterations between reviews, I'm even accustomed to the red button "Changes requested" nowadays

#### Bryan Gin-ge Chen (May 21 2020 at 21:44):

Yes, that seems accurate.

#### Bhavik Mehta (May 21 2020 at 21:50):

If there's other people like Ryan who want to make PRs from existing proofs I have many!

#### Bryan Gin-ge Chen (May 21 2020 at 21:55):

I'd say just PR them all with the label.

#### Jalex Stark (May 21 2020 at 22:04):

I'm significantly more likely to browse your PRs than I am to ask you directly what you've done and convince you to start a PR for part of it

#### Jalex Stark (May 21 2020 at 22:06):

Also if there are orphaned PRs sitting around with your code, then people who are not you can answer "is there code for X" questions with PR links instead of "I heard bhavik worked on that"

Last updated: May 10 2021 at 18:22 UTC