summer program for undergrads

Stream: general

[Jeremy Avigad]

Carnegie Mellon Summer School in Logic and Formal Epistemology:
https://www.cmu.edu/dietrich/philosophy/undergraduate/summer-school/
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]

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]

@Kevin Buzzard :up:

[Kevin Buzzard]

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]

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

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

[Alastair Horn]

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]

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]

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]

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

Then they "close to the fire" so to speak

[Patrick Massot]

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]

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]

Or, if I was lucky, I could sometimes help

[Kevin Buzzard]

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]

This year my aims are slightly higher

[Kevin Buzzard]

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]

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]

And second that they attempt to document their code

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

But it's all I can manage

[Patrick Massot]

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

[Kevin Buzzard]

In particular no cap and sure tell your students

[Kevin Buzzard]

Because you would organise something properly

[Kevin Buzzard]

Whereas I prefer chaos

[Patrick Massot]

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]

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

[Yury G. Kudryashov]

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

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

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

Which yaml file? We have lots of them nowadays

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

No we don't

[Kevin Buzzard]

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]

Talking of which, Ali Sever passed this week

[Bhavik Mehta]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Alex J. Best]

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
- link: https://github.com/alexjbest/fakeproject
  author: Alex
  description: >
    Who's reading this
  status: in progress

[Alex J. Best]

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

[Bhavik Mehta]

Yury G. Kudryashov said:

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

https://github.com/leanprover-community/mathlib/pull/2770 Done

[Patrick Massot]

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

[Bhavik Mehta]

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]

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]

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]

I like the #please-adopt label

[Ryan Lahfa]

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

[Patrick Massot]

This is not the usual situation

[Patrick Massot]

You should rather expect to have quite a bit of work

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Ryan Lahfa]

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]

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]

Yes, that seems accurate.

[Bhavik Mehta]

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

[Bryan Gin-ge Chen]

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

[Jalex Stark]

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]

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"