schedule

Stream: Lean for the curious mathematician 2020

[Jalex Stark]

one question is "ignoring ~all other constraints, what is the most useful sequence of programming to have for ~6 hours a day on ~5 consecutive days," where let's say the objective function is to maximize the probability that each participant either makes a nontrivial PR to mathlib or points to a concrete friction that prevented them from doing so

[Jalex Stark]

I'll post my best-guess answer to this question later today in the form of a tentative schedule. I think @Johan Commelin is forming such a guess independently from me.

[Johan Commelin]

Here's my "timeless" schedule proposal:

Times are all UTC.

Monday 07:00 -- 13:00 :: Tech support + registration
  Getting Lean and VScode up and running.
  Installation videos (prerecorded)
  Volunteers available on Zulip + screensharing.
  Git + github demo (prerecorded talk)
  Make a PR to participants.md that adds your name
  (we can fix all the merge conflicts later)

Monday 13:00 -- 13:30 :: Welcome + 1st Lean proof
  Infinitude of primes?? (using `back`, @Scott?)

Monday 13:30 -- 14:00 :: NNG demo (@Kevin?)

Monday 14:00 -- 15:00 :: NNG "exercise session"

Resources
=========

Make sure that we have an up to date list of helpful resources.

  * Installation page
  * Gitbook

  * NNG
  * Mathematics in Lean


Talk ideas (sorted from "beginner" to "advanced"):
==================================================

What is a Type? What is a Prop? (15 minute talk)
  Top-down approach to type theory for mathematicians

What is a type? What is a set? What is a subtype?
  How to think about them, how to use them.

Set/finset/set.finite whut?
  What's the difference? How to use them?
  How to navigate between them.

Dealing with numbers
  nat subtraction/division
  int division
  norm_cast and friends

Totalizing functions "0¯¹ = 0, shock! horror!" (15 minute talk)
  Why do we totalize functions?
  Why is this not a problem?

What's with all those crazy brackets??
  Explain (), {}, [], {{}} for assumptions
  Explain \<,\> and \f<,\f> for use in terms

Library overview "Algebra" (?)
  Point out that we totalize inv

Library overview "Order" (?)

Library overview "Linear algebra" (?)
Library overview "Topology" (@Reid?)
Library overview "Category theory" (@Scott?)

Analysis "What is a filter?" (@Patrick?) (45 minute talk?)
  Why does mathlib use filters?
  How do you work with filters?

Library overview "Analysis" (?)
Library overview "Measure theory" (?)

Library overview "Geometry" (@Sébastien?)
  Manifolds in Lean.

Library overview "Number theory" (15 minute talk)
  We don't have that much. But the theorems have cool names attached!

Library overview "meta code" (@Rob? @Mario?)

How to write a baby tactic

[Patrick Massot]

I went all the way to the bottom wondering what would be left for Wednesday...

[Johan Commelin]

The pair programming sessions!

[Johan Commelin]

No, this schedule is "timeless" as I said. So we still need to assign timeslots.

[Patrick Massot]

But it does start with a specific schedule for Monday, that's why I was tricked

[Johan Commelin]

Yup, I understand. It's only a draft. And the start is somewhat "canonical"

[Yury G. Kudryashov]

+1 topic: defeq vs provable eq.

[Johan Commelin]

@Yury G. Kudryashov Thanks, good idea. Added to the list: https://github.com/leanprover-community/lftcm2020/blob/master/topics_braindump.md

[Kevin Buzzard]

I can do that as part of a NNG overview

[Kevin Buzzard]

I understand all this much better now. A mathematician thinks of the natural numbers as a specification. But if you want to make NNG then you have to think about the implementation. The two types of equality are some sort of dissonance between these two ways of thinking about things.

[Johan Commelin]

Well... I was thinking maybe we do rather short talks, and then "do one thing, and do it well"

[Johan Commelin]

We have some time, so we can experiment with prerecording some of the basic talks that people may want to watch back

[Scott Morrison]

1st Lean proof Infinitude of primes?? (using back, @Scott?)

I'm happy to do this, or set up the files for someone else to do it.

(With the proviso that in the demo I usually give, the back tactic is totally cheating, and has been fine-tuned for the problem. But it's faking the sort of thing a good hammer will one day do. :-) I can modify this demo to not cheat fairly easily, at the cost of a little extra time, if people would prefer that.)

[Johan Commelin]

Yeah, I think for a workshop like this, it's fine to entice them with a hammer that isn't in mathlib yet, but the hammer shouldn't cheat.

[Patrick Massot]

I tried to work a bit on Johan's schedule. Assuming that we will indeed have a couple of real beginners (or that we want to use the opportunity to record nice videos for beginners) I think we need to have two parallel tracks. The beginner track will have more talks and exercises sessions while more advanced people can do pair coding or follow live coding sessions, or spend even more time on Zulip than usual. And of course people can move freely between those two states (especially for library overview sessions). Johan's schedule can then become the beginner track schedule like this:
I took your schedule draft and tried to turn it into a beginner track. Maybe it's too rigid and school-like.

Monday:

• Monday 07:00 -- 13:00 :: Tech support + registration
  Getting Lean and VScode up and running.
  Installation videos (prerecorded)
  Volunteers available on Zulip + screensharing.
  Git + github demo (prerecorded talk)
  Make a PR to participants.md that adds your name

• Monday 13:00 -- 13:30 :: Welcome + 1st Lean proof Infinitude of primes?? (using back, @Scott?)

• Monday 13:30 -- 14:00 :: NNG demo (@Kevin?)
  *Monday 14:00 -- 15:00 :: NNG "exercise session"

Tuesday:

Morning:

• Top-down approach to type theory for mathematicians
• MIL walkthrough + exercises tutoring, Can we get Jeremy?

Afternoon:

• Set/finset/set.finite whut? What's the difference? How to use them? How to navigate between them.
• Dealing with numbers nat subtraction/division int division norm_cast and friends

Wednesday:

Morning:

• Structures and classes
• What's with all those crazy brackets??

Afternoon:

• Exercices: redo either groups and ring or metric spaces, prove basic lemmas

Thursday:

Morning:

• Library overview "Order", including Galois connections (Kevin, 15 minutes)
• Library overview "Groups and rings" (Johan, 30 minutes)
• Exercices on order, groups and rings, maybe redo lattice structure on subgroups?

Afternoon:

• Library overview "Number theory" (Do we actually have any number theory in mathlib?, 0 minutes)
• Library overview "Linear algebra" (Anne, 20 minutes)
• Library overview "Category theory" (Scott, 8 hours)
• Exercices in linear algebra and category theory

Friday:

Morning:

• Library overview "Topology", including filters (Patrick, 45 min)
• Library overview "Calculus and analysis" (Sébastien, 30 minutes)

Afternoon:

• Library overview "Measure theory and integration" (Yury, 15 minutes)
• Library overview "Geometry" (Sébastien, 30 minutes)
• Library overview "meta code" (Rob, 1 hour)
• Exercices

[Yury G. Kudryashov]

I'm not sure that I can do a good overview of the measure theory library. I mean, most of my contributions were outsidef of measure_theory/.

[Patrick Massot]

I forgot to mention that names are only dreams, nobody promised anything.

[Patrick Massot]

My not so secret hope about measure theory is that you will return to adopting Joe's PR in the mean time. That would make you our integration expert.

[Patrick Massot]

I only hope that wouldn't bring the measure theory curse on you (everybody touching measure theory in mathlib mysteriously disappear).

[Yury G. Kudryashov]

The main reason I didn't come back to this is that every time I look at this library I want to refactor it.

[Yury G. Kudryashov]

Then I decide to postpone the refactor, and do something simpler.

[Yury G. Kudryashov]

(and @Sebastien Gouezel doesn't like my idea of making measures {}/() not [] arguments)

[Johan Commelin]

@Patrick Massot Thanks a lot for turning my first sketch into something reasonable.
I like the idea of two tracks.

[Johan Commelin]

For the beginner track, I think it would be really useful if we (pre)record the talks. It's quite likely that people will want to watch the talks at a later stage as well.

[Patrick Massot]

Yes, that's what I meant, especially since we don't know whether there will be beginners that week.

[Patrick Massot]

The big question is should we slice those talks in ten minutes youtube slices or do we simply record normal lectures.

[Sebastien Gouezel]

Yes, the measure space refactor is a tricky question. I have the impression that, in many cases, we have a canonical measure on a space, and then having it as a typeclass is really the most convenient thing (especially when building the integral). But it is also true that in some situations you will have several measures that you will want to compare on the same space (e.g. Lebesgue and Gaussian measure on $\mathbb{R}^n$), and writing @ on all theorems will be painful. Could we have a notation for the integral, in terms of an explicit measure, defined in terms of @integral...?

[Sebastien Gouezel]

I'm definitely open to discussion, anyway!

[Sebastien Gouezel]

A solution could be to have a notation for the integral picking the measure from a typeclass, another notation for the integral with an explicit measure, and having the measure as an implicit parameter in the theorems: then the theorem would apply to both notations, and would pick the right measure by unification.

[Alena Gusakov]

Are any of the talks going to be recorded? I don't plan to make it to the Monday morning sessions but I would like to see the type theory talk, as well as some of the library overview talks, and if they're 7-8am UTC it'll be like 3-4am for me lol

[Patrick Massot]

Yes, the hope is to record the beginner talks.

[Alena Gusakov]

Cool, thank you!

[Patrick Massot]

We probably need to get people listed in the schedule to actually say whether they'd like to give those talks/exercises sessions. @Scott Morrison, @Rob Lewis, @Jeremy Avigad, @Anne Baanen, @Sebastien Gouezel, @Yury G. Kudryashov do you like what you see in this schedule? Note that the indicated lengths are pretty random.

[Kevin Buzzard]

I assume you're not asking me because you know already I'll just say "yes" :-)

[Jeremy Avigad]

For some reason, I didn't know about this thread. I am still catching up on it, but yes, I'll be happy to help out any way I can. (I just checked my calendar, and I am free that week. What are the odds?)
Patrick, what did you have in mind for the MIL walkthrough?
BTW, I took a break from working on another project (and old-fashioned pen-and-paper logic textbook I am writing), but I have reached a resting point there, and I am planning to get back to MIL this week.

[Patrick Massot]

Kevin Buzzard said:

I assume you're not asking me because you know already I'll just say "yes" :-)

Your answer has been type-checked by automation.

[Kevin Buzzard]

My term will essentially be over by Wed so I will be back in MIL mode too.

[Patrick Massot]

Great, going back to MIL is also on my agenda for the coming week.

[Patrick Massot]

Note that the schedule is very flexible. Anyone who is willing to help can decide a lot.

[Patrick Massot]

What we need right now is to be able to confirm for sure that this thing will happen. It was originally planned as a physical gathering in Freiburg, but has gone online with the virus. It's in one month so we need to tell people who originally registered that something will happen, and we need to communicate more. But first we need to make sure we'll have lecturers.

[Jeremy Avigad]

Great. I am happy to do anything. I can give a bottom-up introduction along the lines of MiL, or a top-down one along the lines of TPiL.

It's hard to teach interactive theorem proving in a week -- people need time to experiment and digest. But maybe we can try a format where we give people time to work on exercises and ask questions (in breakout rooms? in a chat window?) and then talk about them.

I'll think about it...

[Rob Lewis]

Am I expected to do a live talk or live discussion or to record something? Anything's fine as long as I have some prep time.

[Patrick Massot]

It's up to you I think. Both prerecord talks and live talks have advantages and disadvantages.

[Patrick Massot]

Actually the meta talk is pretty special because it will be useful for a broad range of people. There are lots of intermediate or advanced users that have no clue about tactic writing.

[Patrick Massot]

Jeremy, I know teaching intereactive theorem proving in one week is hard. The hope is to give a kick start. And indeed I imagine half of the time being devoted to exercises sessions. Hopefully we can have enough mentors to take care of both the beginners and some intermediate users who won't want to do the exercises but will want to ask more questions that week.

[Jeremy Avigad]

Sounds good! I am at your disposal.

[Sebastien Gouezel]

I can certainly talk on the geometry library (and it would motivate me to clean some rough edges beforehand), but not on Friday. I think it would be a good idea to let Yury talk on the analysis library.

[Johan Commelin]

I will try to design a talk on "groups and rings" next week, and record it. After that, I can share my experience (software setup, etc...) and you can burn down the talk (-;

[Johan Commelin]

@Patrick Massot I interpret "groups and rings" as "everything between semigroup and field".

[Yury G. Kudryashov]

Are there any plans for "non-beginner" track?

[Patrick Massot]

I think the plan is to have virtual pair programming

[Patrick Massot]

Sebastien Gouezel said:

I can certainly talk on the geometry library (and it would motivate me to clean some rough edges beforehand), but not on Friday. I think it would be a good idea to let Yury talk on the analysis library.

There is really no way we can discuss differential geometry before Friday. This is the supr of mathlib, it needs absolutely everything else. Do you still get motivated to clean the rough edges if someone else (@Heather Macbeth maybe?) is presenting it?

[Heather Macbeth]

Hi Patrick, thank you for the implied invitation, but I really don't know anything about the differential geometry library! I am hoping this will soon change, of course.

[Patrick Massot]

Exactly, I propose this should change before July 20th.

[Heather Macbeth]

I am happy to do some task for this workshop. But I myself would learn a lot from hearing Sebastien talk about the structure and design choices of the differential geometry libraries, and I would be sorry if that talk did not happen :)

[Patrick Massot]

The issue is that Sébastien won't be available on Friday, and we need everything else before discussing it.

[Sebastien Gouezel]

(deleted)
It turns out I could free some time on Friday afternoon finally!

[Patrick Massot]

Sébastien... you're ruining my plot to get Heather up to speed.

[Sebastien Gouezel]

OK, let's fix it.

[Patrick Massot]

Plan B: you'll need a TA for the exercise session, what about Heather?

[Sebastien Gouezel]

What exactly do you mean by "exercise session"? :)

[Patrick Massot]

Each session will have a short presentation followed by a long exercise session. On Thursday and Friday sessions will be devoted to specific areas of mathlib. We won't rebuild the definitions, but the exercises can be reproving lemmas that are already in mathlib.

[Heather Macbeth]

Sure, I can do that.

[Rob Lewis]

Maybe easier to discuss here than in the PR you just made -- I'm confused about how 4.5 hours on metaprogramming fits into the Monday schedule. There's no way to address that to people who aren't already somewhat comfortable with non-meta programming (= proving).

[Kevin Buzzard]

Many mathematicians will never learn anything about metaprogramming. Hardly anyone does it at Xena

[Johan Commelin]

I think that the meta session is for participants that have already been hanging out on Zulip for several months...

[Johan Commelin]

The PR that Rob was talking about: https://github.com/leanprover-community/lftcm2020/pull/8/files

[Johan Commelin]

@Kevin Buzzard @Jeremy Avigad @Yury G. Kudryashov @Sebastien Gouezel @Rob Lewis @Anne Baanen @Scott Morrison please leave comments (-; :octopus:

[Johan Commelin]

And all other people that are interested in contributing one way or another.

[Anne Baanen]

I saw I was in the old schedule for linear algebra. I'm happy to prepare for that, but if someone else wants to volunteer who has mathematical experience with linear algebra past a couple of undergrad courses, I would like to nominate them :)

[Johan Commelin]

I think it would be great if you do it!

[Johan Commelin]

We just turned it to TBA because we hadn't heard back yet. But changing TBA to AB isn't that hard (-;

[Johan Commelin]

Feel free to suggest a change on the PR :grinning_face_with_smiling_eyes:

[Patrick Massot]

Sorry I missed the conversation, I opened the PR and then went getting my daughters at school.

[Patrick Massot]

Johan converted the schedule to HTML tables. I suspect he simply wanted to play with cool markdown syntax, but the bad side is people then don't read surrounding text...

[Patrick Massot]

Also, I opened the PR while discussing with Johan, but I intended to also explain it to other people.

[Patrick Massot]

The main change is I decided that having planned boundaries between talks and exercises sessions was only getting in our way. So It's not that we suddenly expect people to prepare super long lectures. We still hope that most "lectures" will be short, say half an hour for topic lectures, but then there will be long exercises sessions, as explained in the text surrounding the tables.

[Patrick Massot]

Of course everybody accepting to help still has full freedom to handle things in whatever sounds best.

[Patrick Massot]

The afternoon end-time are completely open-ended. Serious participants will continue working in the evening anyway.

[Johan Commelin]

Right, we will secretly keep track of who is online during the night hours. Those participants will receive invitations to become regular mathlib contributors at the end of the week.

[Patrick Massot]

I merged the PR because it doesn't make sense to look at the diff. The goal is to send announcement emails this week-end, so we need to know whether everybody is happy with the plan. The website has exactly four pages, two of which are very short, so everybody should be able to read everything easily.

[Patrick Massot]

My idea for the meta-programming session is indeed to target people who are already mathlib users. The beginner track is already very ambitious, I don't think you can add meta-programming on top of that. So I made it a parallel session, and I moved it early so that some people can attend both this session and the topical sessions on Thursday and Friday.

[Patrick Massot]

My idea for this meta-programming session was to cover the content of the tactic writing tutorial plus some discussion of expr juggling, and then have people (re-)writing baby tactics. But of course Rob is free to do whatever he thinks is best, or trying Gabriel to do it or whatever. Johan and I are trying to push this thing so that it actually happen, but we have no dictator dreams here.

[Chris Hughes]

Can the tactic writing tutorial cover what a metavariable is? I never understood what assigned and instantiated metavariables are.

[Rob Lewis]

I can try!

[Patrick Massot]

Note also we are currently missing speakers, especially on Wednesday. Talks on Wednesday are not specialized, so hopefully we'll get volunteers. Also I put my names in two slots but I won't fight back if someone wants to replace me.

[Alex J. Best]

I'm happy to speak on something, if you want !

[Patrick Massot]

Do you see any slot you'd like to fill?

[Patrick Massot]

Maybe I should paste the url again: https://leanprover-community.github.io/lftcm2020//schedule.html

[Alex J. Best]

Of the three TBA's I see "structures and classes" for sure, though rebuilding a topological hierarchy also sounds fun.

[Patrick Massot]

Great! It would be nice if you could prepare the topological hierarchy building stuff. For the two Wednesday afternoon sessions, my idea is the main speaker will prepare a sparse Lean file skeleton, maybe with a lot of comments informally describing the intended math content, comment a bit on the skeleton in the beginning (either live or prerecorded) and then help participants turn it in an actual Lean file.

[Patrick Massot]

So the first task would be to prepare the solutions file, and then make the exercise file out of it. The solution file can copy-paste mathlib content but not too much, we still want simplified versions.

[Patrick Massot]

Ideally, we would even have an intermediate solution file with (small) design issues, and then a better one.

[Patrick Massot]

For instance the topology building session could first do metric spaces and topological spaces separately, hit the standard issues and switch to forgetful inheritance.

[Alex J. Best]

Sounds good, thanks! I'll get preparing then.

[Bhavik Mehta]

I'm also happy to speak on something if necessary

[Patrick Massot]

Do you know about measure theory and integration in mathlib?

[Bhavik Mehta]

Nope

[Patrick Massot]

It was worth a shot.

[Alex J. Best]

Now that the schedule is getting there what do people think of adding lftcm to https://researchseminars.org/ at some point in the next few days for more exposure.

[Patrick Massot]

The goal of the current organization push is indeed to allow more advertisement. We haven't discussed specific advertising plans though.

[Kevin Buzzard]

Patrick I will give as many talks as you think are reasonable and I will actually prepare them.

[Patrick Massot]

I already assigned quite a few to you.

[Kevin Buzzard]

I don't know anything about measure theory and integration though :-)

[Patrick Massot]

Of course I'm reusing existing stuff. I'm using that worked on the NNG and CNG.

[Patrick Massot]

The only slightly exotic assignment is orders.

[Patrick Massot]

That's because you once told me you enjoyed putting a lattice structure on subgroups or something like this.

[Yury G. Kudryashov]

You can assign integration to me

[Kevin Buzzard]

Ha ha! The last time I put a lattice structure on subgroups was about 5 hours ago! I did this on the twitch stream and at Xena earlier tonight

[Floris van Doorn]

Is there another slot that needs to be filled?

[Floris van Doorn]

Oh, I see Structures and classes, but that's 4 at night EDT...

[Jeremy Avigad]

Sorry I have been AWOL, but the schedule looks great, and I am happy to do the things that were assigned to me.

[Johan Commelin]

Floris van Doorn said:

Oh, I see Structures and classes, but that's 4 at night EDT...

I think we can still move things around a little bit.

[Johan Commelin]

Well, actually... maybe it's not so easy to move things around anymore.

[Johan Commelin]

@Floris van Doorn But you are very welcome to hang around on Zulip during the exercise sessions and help with answering questions, or to lead some pair/triple programming sessions

[Floris van Doorn]

I'm happy to do that!

[Johan Commelin]

Great, thanks!

[Patrick Massot]

Floris van Doorn said:

Oh, I see Structures and classes, but that's 4 at night EDT...

I think it would be great if you could give that one. An option would be to record your talk in advance and prepare the exercises, but have other people helping participants to do the exercises. This is the talk that need the greatest expert, at least if you remove the meta-programming talk which requires different expertise.

[Miguel Raz Guzmán Macedo]

Hello all!
I think I will be joining the afternoon sessions for most of the LFTCM2020 (I'm based in Mexico).
Thanks for opening this up! I just made my PR to add myself as a particpant! :party_ball:

[Yury G. Kudryashov]

I've just realized that I'll need a lot of coffee on Friday morning.

[Yury G. Kudryashov]

Because my first talk starts at 5am local time

[Johan Commelin]

@Yury G. Kudryashov My kids still occasionally wake me up at 5am. How did you train them not to do that? :stuck_out_tongue_wink:

[Patrick Massot]

Oops, Jeremy complained so we moved him to the afternoon, but we didn't go as far as thinking about who else could have this problem... I don't think we want a zombie Yury lecturer. We need to think about moving things around.

[Patrick Massot]

Actually we allocated half the afternoon to measure theory and integration but I'm not sure we have so much to show in this direction, especially if the ongoing integration refactor and FTC doesn't land before the workshop. What about spending all morning on topology and having a first afternoon session about calculus + integration?

[Yury G. Kudryashov]

Can we decide this Thursday? I'll see if I can PR the refactor by Friday.

[Patrick Massot]

I'm happy to decide this whenever you want. I'd be very happy to see this moving, but I really don't want you to feel force to wake up at 4am and be a zombie all day.

[Danila Kurganov]

How up-to-date are the times for this on https://researchseminars.org/seminar/LeanCurious ? It looks quite a bit different from the schedule I see way up above (where should I pay attention to know the event times?)

[Alex J. Best]

Researchseminars will always display in your local time for one.

[Alex J. Best]

Are you comparing it to https://leanprover-community.github.io/lftcm2020/schedule.html ? That page is the most correct schedule.

[Johan Commelin]

@Danila Kurganov This thread contains a lot of discussion/planning, so it probably contains data that is no longer accurate. The time schedule over at https://researchseminars.org/seminar/LeanCurious should be exactly the same as the schedule on https://leanprover-community.github.io/lftcm2020/schedule.html (modulo timezone computations). If you see a difference, please let me know!
The second link contains the authoritative schedule.

[Andrew Sutherland]

@Johan Commelin Do you mind if I add chat links to this stream to the events listed on researchseminars.org?

[Johan Commelin]

@Andrew Sutherland Sounds good! Please go ahead.

[Johan Commelin]

I don't really know what such chat links are, but links never hurt.

[Johan Commelin]

Also: welcome! :hello:

[Andrew Sutherland]

@Johan Commelin Done! I you click on the titles of any of the events listed on https://researchseminars.org/seminar/LeanCurious you will see a "chat" hyperlink in parentheses that links here (this link also appears on the homepage for each talk (like this one for example). This will make it easier for people who discover this workshop on researchseminars.org as I did to find their way here.

You can also attach links to slides, papers, pre-recorded videos, and live streams to any of the talks. These are useful not only during the workshop but also afterward for people who might have missed it or want to go back and revisit something (for example, here is a list of talks and available content related to the online ANTS conference that took place last week).

[Andrew Sutherland]

BTW, as the organizer you can send speakers links that will let them edit and add content to their talk listings on researchseminars.org using the link listed at the top of each "Edit talk" page.

[Johan Commelin]

@Andrew Sutherland Thanks a lot. We plan to record everything, and upload to youtube. Once that is done, we can add links on researchseminars.org as well.

[Andrew Sutherland]

Sounds good!

[Philip Vetter]

@Johan Commelin Where is the livestream?

[Johan Commelin]

@Philip Vetter It will start in a moment. Note that talks only start in the afternoon.

[Johan Commelin]

The morning is dedicated to getting a working installation of Lean on everyones computer.

[Philip Vetter]

When and where would the Zoom link be posted? I have not noticed any email message.

[Johan Commelin]

The link will be posted here and on the conference website