pair/triple programming

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

If you want to be tutor in a pair/triple programming session during this workshop, please leave a ping here.
The idea would be that one or two beginners try to write some lean code in an area that interests them.
The tutor should judge whether the topic is suitable for the experience level of the participant. (Intermediate users could dabble in tactic writing, or tricky definitions, but beginners probably shouldn't.)

A group can then start a video call with screen sharing, and discuss the code as they are writing it.

[Danila Kurganov]

When do these pair-programming sessions start? If it's anytime could I get someone for a bit before the 'first' talk to help define something? I'm pretty beginner

[Johan Commelin]

@Danila Kurganov Sure, please join Zoom

[Danila Kurganov]

@Johan Commelin I'm on the zoom, i'll wait until zoom things are fixed for this?

[Anne Baanen]

The Zoom meeting for pair programming has started:
Topic: LftCM Pair Programming
Time: This is a recurring meeting Meet anytime

Join Zoom Meeting
https://vu-live.zoom.us/j/99558325939?pwd=VnR6TWMwblRKeUE5a2k5cE81YlhTUT09

Meeting ID: 995 5832 5939
Password: 649721

[Thomas Eckl]

I would be very grateful if someone knowing the formalization of perfectoid spaces pretty well can show me which lemmas need to deal with isomorphisms of localized rings, a problem that Kevin Buzzard highlighted in his Edinburgh talk on the project last year. I am not sure what's the best way to find such lemmas: Use search tools in Lean? Other search tools? Just find my way through the code myself?

Actually, Kevin's remarks prompted me to think about the usefulness of HoTT for problems like this. I started formalizing things in Lean 2, and now put the code on GitHub : https://github.com/theckl/HoTT-Case-Study , together with an extensive Readme file about the details of the project and the philosophy behind it (including a suggestion how to use HoTT in fashionable mathematics!).

Note that I am an Algebraic Geometer (from the primordial soup) usually working on problems (yet) far away from formalization. So I tick some of the boxes of the intended audience and hope that I am allowed to ask these HoTT-related questions in this conference, despite Johan's initial warning yesterday.

[Johan Commelin]

Hey @Thomas Eckl that's certainly allowed (-;

[Johan Commelin]

But just maybe not during the Zoom talks (-;

[Johan Commelin]

But I would love to talk about this :thumbs_up:

[Thomas Eckl]

OK, sorry, and thanks. Let me know when there is a good time for you; I guess as one of the organizers you are quite busy ...

[Johan Commelin]

Yeah, that's certainly true

[Johan Commelin]

Also, I think the schemes formalisation already contains the sort of "problem/solution" you are interested in

[Johan Commelin]

So that might actually be a better use case

[Johan Commelin]

I'm sure Kevin will be delighted to show you around, but he also has a talk tomorrow

[Thomas Eckl]

I can certainly wait until Thursday.

[Johan Commelin]

Cool!

[Thomas Eckl]

@Johan Commelin Thanks for your hint to the formalisation of schemes. I downloaded Ramon Fernandez Mir's project and used the search tools that you showed us on Wednesday - participating in the conference pays off! ;-) I think I know now where to find all the little lemmas on isomorphisms of localizations: not too surprisingly in the construction of the structure sheaf.

I stiil would love to hear opinions of Lean 3 users on HoTT. Maybe we can arrange a meeting after the conference, when you are not so busy. Or is the modern way to discuss a chat in Zulip?

[Thomas Eckl]

@Scott Morrison You liked my contribution above. Does it contain a particular topic that you are interested in? I liked a lot your presentation on categories yesterday afternoon. This is getting close to a tool that you can use in actual research ...

[Scott Morrison]

Mostly it was just intended as a friendly welcome!

[Scott Morrison]

I'm happy to see algebraic geometers using Lean. I'm not exactly a category theorist -- my background is in quantum topology / tensor categories / subfactors.

[Kevin Buzzard]

@Thomas Eckl I would be very interested to see a basic definition of algebraic geometry up to and including a definition of a scheme, and a proof that affine schemes are schemes, in a HoTT theory.

[Kevin Buzzard]

If you want to go further, then there is an exercise in Hartshorne's book on algebraic geometry about gluing sheaves on open subsets of a topological space (basically showing that if the sheaves on the open subspaces agree on overlaps and the isomorphisms satisfy a cocycle condition then they can be glued to make a sheaf on the whole space which agrees with the original sheaves when restricted to the open subsets). Kenny Lau did this exercise in Lean and it was hard work, but possible.

[Kevin Buzzard]

My original development of schemes had a huge design flaw which I worked around because I was determined to get it to work. I supervised Ramon's MSc project on schemes and he did it in a much better way, using universal properties of localisations rather than the concrete definition; this is somehow a crucial insight.

[Kevin Buzzard]

I am still very unclear about whether my original approach would have worked much more easily in a HoTT theory, but I am not even sure that it is the right approach.

[Thomas Eckl]

I am not exactly sure what your original approach was, but I liked a lot Ramon's project. Maybe I can extend my little project on formalization to a complete formalization of schemes and thus comply with your wishes. But it may also very well happen that I have to admit the unsuitability of HoTT for such efforts - but then I should at least understand better why.

[Kevin Buzzard]

This is the kind of question I would really have loved to talk to Voevodsky about :-(