Zulip Chat Archive

Stream: general

Topic: summer program for undergrads


view this post on Zulip Jeremy Avigad (Feb 10 2020 at 18:20):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 06 2020 at 10:48):

@Kevin Buzzard :up:

view this post on Zulip 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 :-)

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (May 06 2020 at 11:46):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 06 2020 at 14:53):

Then they "close to the fire" so to speak

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2020 at 14:58):

Or, if I was lucky, I could sometimes help

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2020 at 14:59):

This year my aims are slightly higher

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:02):

And second that they attempt to document their code

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:03):

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

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:03):

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

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:04):

But it's all I can manage

view this post on Zulip Patrick Massot (May 21 2020 at 15:04):

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

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:04):

In particular no cap and sure tell your students

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:04):

Because you would organise something properly

view this post on Zulip Kevin Buzzard (May 21 2020 at 15:05):

Whereas I prefer chaos

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 21 2020 at 15:08):

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

view this post on Zulip 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).

view this post on Zulip Patrick Massot (May 21 2020 at 18:03):

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

view this post on Zulip 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)".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 21 2020 at 19:20):

Which yaml file? We have lots of them nowadays

view this post on Zulip Kevin Buzzard (May 21 2020 at 19:21):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2020 at 19:23):

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

view this post on Zulip Patrick Massot (May 21 2020 at 19:23):

No we don't

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 21 2020 at 19:26):

Talking of which, Ali Sever passed this week

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 21 2020 at 19:28):

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

view this post on Zulip Yury G. Kudryashov (May 21 2020 at 19:29):

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

view this post on Zulip 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:

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

view this post on Zulip Alex J. Best (May 21 2020 at 19:32):

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

view this post on Zulip 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:

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

view this post on Zulip Patrick Massot (May 21 2020 at 19:41):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ryan Lahfa (May 21 2020 at 21:29):

I like the #please-adopt label

view this post on Zulip Ryan Lahfa (May 21 2020 at 21:29):

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

view this post on Zulip Patrick Massot (May 21 2020 at 21:30):

This is not the usual situation

view this post on Zulip Patrick Massot (May 21 2020 at 21:30):

You should rather expect to have quite a bit of work

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (May 21 2020 at 21:44):

Yes, that seems accurate.

view this post on Zulip 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!

view this post on Zulip Bryan Gin-ge Chen (May 21 2020 at 21:55):

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

view this post on Zulip 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

view this post on Zulip 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