Zulip Chat Archive

Stream: general

Topic: LUG Freiburg 2018


view this post on Zulip Johan Commelin (Sep 11 2018 at 07:23):

Hi everyone, I am organising a Lean User Group meeting in Freiburg (Germany). Dates: Monday 5 November – Wednesday 7 November.
I would like to mimic the model of the very succesful meeting in Orsay. So it will be a free-form hackathon with some spontaneous talks. Nevertheless it may be useful to broadly sketch a topic: I would like to use this workshop to work on mathematical topics revolving around geometry, algebra and number theory (e.g., manifolds, schemes, homological algebra, number fields, and any category theory that shows up along the way). Besides that we can also discuss and improve tactics/automation that will streamline our work.
There is limited funding to cover hotel/travel costs.

If you would like to join in this workshop, please reply to this thread while mentioning me (with an @).

view this post on Zulip Patrick Massot (Sep 11 2018 at 07:28):

@Johan Commelin I'll come

view this post on Zulip Johannes Hölzl (Sep 11 2018 at 08:49):

@Johan Commelin I'll come too

view this post on Zulip Kenny Lau (Sep 11 2018 at 14:36):

@Johan Commelin I'll come if I can sort it out with my university

view this post on Zulip Kenny Lau (Sep 11 2018 at 14:37):

@Kevin Buzzard how does this work?

view this post on Zulip Kevin Buzzard (Sep 11 2018 at 14:47):

The best thing to do is to keep it quiet and not announce that you will be taking three days off in the middle of term on a public forum. That way nobody will notice.

view this post on Zulip Kenny Lau (Sep 11 2018 at 14:56):

I see

view this post on Zulip Cyril Cohen (Sep 13 2018 at 14:19):

@Johan Commelin I am interested in coming.

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:26):

Cool! I'm looking forward to meeting you.

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:18):

Ok, I've passed your email addresses on to our secretary. You should receive an email soon, with details about hotel and/or travel reimbursements.

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:18):

Don't book a hotel yourself. Our uni will do that for you.

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:19):

@Patrick Massot @Johannes Hölzl @Kenny Lau @Cyril Cohen :up:

view this post on Zulip Tobias Grosser (Sep 14 2018 at 10:51):

@Johan Commelin I had to think a bit about this, but am also very interested in coming.

view this post on Zulip Tobias Grosser (Sep 14 2018 at 10:51):

Seems things could work out.

view this post on Zulip Cyril Cohen (Sep 14 2018 at 10:57):

Ok, I've passed your email addresses on to our secretary. You should receive an email soon, with details about hotel and/or travel reimbursements.

Woah great :)

view this post on Zulip Tobias Grosser (Sep 14 2018 at 11:50):

@Johan Commelin , anything specific you need from my side?

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:54):

No, I think it's fine now. Our secretary will contact you somewhere next week.

view this post on Zulip Johan Commelin (Sep 18 2018 at 08:26):

Our secretary just informed me that she has booked hotel rooms for you. You should get an email with details anytime soon.

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 08:54):

I got the mail

view this post on Zulip Cyril Cohen (Sep 18 2018 at 09:09):

I got it too, thanks! Would you know at what time the meeting ends on wednesday?

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:09):

Whenever you want to leave :lol: No fixed closing times.

view this post on Zulip Johan Commelin (Sep 18 2018 at 09:09):

We could discuss what most people are planning to do, in this thread...

view this post on Zulip Johannes Hölzl (Sep 18 2018 at 09:43):

On Wednesday I will leave around 16h from the station (this is the only direct connection Freiburg -> Amsterdam)

view this post on Zulip Rob Lewis (Sep 18 2018 at 09:53):

Then I assume I'll be on the same train as Johannes.

view this post on Zulip Patrick Massot (Sep 19 2018 at 12:42):

Our secretary just informed me that she has booked hotel rooms for you. You should get an email with details anytime soon.

I think I didn't get anything

view this post on Zulip Patrick Massot (Sep 19 2018 at 12:43):

@Johan Commelin

view this post on Zulip Johan Commelin (Sep 19 2018 at 13:07):

@Patrick Massot I asked the secretary to resend the email.

view this post on Zulip Patrick Massot (Sep 19 2018 at 13:08):

To which email address?

view this post on Zulip Cyril Cohen (Sep 24 2018 at 15:31):

Hi everyone! On Wednesday I will depart at 15:55 from the airport (this is the only flight back to Nice), I guess I will need to leave Freiburg arount 13:00?
@Johan Commelin Would you know a reliable way to go from BSL EuroAirport to Freibourg kind of late on Sunday evening (the plane lands at 22:10 if it is not late)?

view this post on Zulip Johan Commelin (Sep 24 2018 at 15:37):

@Cyril Cohen I think it should be possible to go from the airport to Basel's train station. And from there I expect regular trains to Freiburg till at least midnight. But I don't have any experience with this...

view this post on Zulip Cyril Cohen (Sep 24 2018 at 15:51):

@Johan Commelin Ok, thanks, I'm looking into it.

view this post on Zulip Patrick Massot (Sep 24 2018 at 17:32):

:thinking: Johan told me the airport was unusable, so I took train tickets

view this post on Zulip Cyril Cohen (Sep 25 2018 at 06:53):

@Patrick Massot From Nice I do not have much choice: the shortest train ride is still almost 9h long... so I'd rather fly to a unusable airport :joy:

view this post on Zulip Kenny Lau (Oct 03 2018 at 22:23):

what are the starting/ending times?

view this post on Zulip Johan Commelin (Oct 04 2018 at 06:38):

Well, there is no strict schedule. But in Orsay we used to start at around 09.00 AM. (That is Central European Time, for those of us used to Hong Kong time zones). I think you should go for dinner earlier than in Paris. The German restaurants aren't used to people coming for dinner after 20.00. On Wednesday you should just leave whenever your travel schedule requires you to go.

view this post on Zulip Johan Commelin (Oct 23 2018 at 13:29):

The first week of November is rapidly approaching. In the initial post in this thread, I outlined what I thought would be nice topics for this meeting.

I would like to use this workshop to work on mathematical topics revolving around geometry, algebra and number theory (e.g., manifolds, schemes, homological algebra, number fields, and any category theory that shows up along the way). Besides that we can also discuss and improve tactics/automation that will streamline our work.

@Tobias Grosser has indicated that he would like to work on Presburger arithmetic. Some people in the department have shown some interest, and might want to drop by. So it we might have to showcase the proof of the infinitude of primes a couple of times (-; If there are other things that people would like to coordinate or prepare in advance, I think now would be a good time to discuss it.

view this post on Zulip Johan Commelin (Oct 23 2018 at 13:30):

I can also announce the room where we will be meeting: SR 232 (II. OG/Stochastik). My office is in room 425.

view this post on Zulip Rob Lewis (Oct 23 2018 at 13:54):

What time are people planning to get in on Sunday? I'll be in Strasbourg that weekend and it looks like there are plenty of connections. Should we plan on dinner Sunday night?

view this post on Zulip Johan Commelin (Oct 23 2018 at 13:57):

I can also announce the room where we will be meeting: SR 232 (II. OG/Stochastik). My office is in room 425.

Maybe I should also mention which building :lol:
It's the mathematics institute: Ernst–Zermelo Straße 1. map

view this post on Zulip Johan Commelin (Oct 23 2018 at 13:57):

This is a 5-minute walk from the main station.

view this post on Zulip Tobias Grosser (Oct 23 2018 at 17:18):

I will be around 16:00 in Freiburg.

view this post on Zulip Tobias Grosser (Oct 23 2018 at 17:18):

Would be great to meet for dinner.

view this post on Zulip Tobias Grosser (Oct 23 2018 at 17:19):

Yes, I would very much like to discuss Presburger arithmetic.

view this post on Zulip Tobias Grosser (Oct 23 2018 at 17:20):

Just to get an idea, who would be interested in discussing decision procedures for Presburger arithmetic?

view this post on Zulip Tobias Grosser (Oct 23 2018 at 17:21):

In case there is some interest, I could try to prepare a small documents of things I would like to discuss and potentially useful paper references.

view this post on Zulip Johan Commelin (Oct 24 2018 at 04:02):

I am certainly interested in understanding the roadmap. I'm probably not really qualified for in-depth contributions.

view this post on Zulip Johan Commelin (Oct 31 2018 at 18:20):

Just wanted to let the other participants know that @Michael Jendrusch from Heidelberg is also joining!

view this post on Zulip Johan Commelin (Nov 02 2018 at 13:43):

I just checked out the room (232) that we will be in. There are two blackboards, a whiteboard and a projector (beamer). There is a VGA cable, but I didn't see an HDMI cable. There are plenty wall sockets. (If you want to showcase something, and you need HDMI, please take your own cable with you. Otherwise, I can try to find one somewhere.)

view this post on Zulip Kenny Lau (Nov 03 2018 at 22:40):

Should we meet on Sunday as well?

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 08:31):

Yes, we can meet! I guess I will be in Freiburg in the early afternoon. Rob should be at the hotel at 7pm.

view this post on Zulip Patrick Massot (Nov 04 2018 at 11:10):

I'll arrive at 9pm, so I guess we'll meet tomorrow morning. Are we all in the same hotel? I'm at Apart Hotel Mathildenstraße 14. Do we have a starting time tomorrow morning?

view this post on Zulip Johan Commelin (Nov 04 2018 at 11:41):

I live in a little village south of Freiburg, so I won't meet you today. I'll be at the institute tomorrow morning at 8.30. I'm fine with starting at 9.00, like in Orsay.

view this post on Zulip Tobias Grosser (Nov 04 2018 at 12:10):

I will be there from 5ish. Happy to go for dinner

view this post on Zulip Kenny Lau (Nov 04 2018 at 12:46):

I might arrive on monday

view this post on Zulip Tobias Grosser (Nov 04 2018 at 13:06):

@Kenny Lau, is this last-minute booking?

view this post on Zulip Kenny Lau (Nov 04 2018 at 13:38):

mostly

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 14:24):

@Tobias Grosser we can meet for dinner at around 7pm? Then @Rob Lewis is also in Freiburg.
@Patrick Massot I'm also at the Apart Hotel.

view this post on Zulip Tobias Grosser (Nov 04 2018 at 14:38):

I am also at Apart Hotel. @Johannes Hölzl, should we meet in the lobby at 19:00?

view this post on Zulip Patrick Massot (Nov 04 2018 at 15:06):

Johan, I don't mind starting at 9 but your memories are wrong, in Orsay we started at 10 on the first day.

view this post on Zulip Patrick Massot (Nov 04 2018 at 15:10):

Johannes, I guess I'll see you during breakfast around 8:30 then.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 15:22):

Johan, I don't mind starting at 9 but your memories are wrong, in Orsay we started at 10 on the first day.

Surely all we can deduce is that _someone's_ memories are wrong...

view this post on Zulip Johan Commelin (Nov 04 2018 at 15:34):

I am quite sure that my memory is wrong. If I recall correctly, that happens quite often to me.

view this post on Zulip Michael Jendrusch (Nov 04 2018 at 17:02):

Hi, I'm also joining the workshop and though I suppose I'm quite late with introductions, I'll introduce myself either way.
I'm Michael, a student from Heidelberg. I am mostly doing machine learning on medical and biological imaging data (I come from a CS / biology background). I've started learning Lean a while ago (and have been lurking on Zulip for some time) for a project where we're formalizing biological protocols on top of microfluidic devices in terms of (symmetric monoidal) categories, so I'm trying to wrap my head around code generation and proof automation for defining types representing symmetric monoidal categories in terms of some generating objects and morphisms.

Anyway, I've arrived at the Hotel in Freiburg and I'm looking forward to the workshop.

view this post on Zulip Kevin Buzzard (Nov 04 2018 at 18:13):

Can you just explain (to a pure mathematician) what biology has to do with symmetric monoidal categories? I last went to a biology class about 30 years ago by the way.

view this post on Zulip Patrick Massot (Nov 04 2018 at 20:41):

I love hotels having eduroam wifi!

view this post on Zulip Patrick Massot (Nov 04 2018 at 20:42):

and the German touch: the room has the standard water boiler and a beer bottle opener

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 21:18):

Hm, there is no eduroam in my room :-( I need to write down passwords, like a caveman

view this post on Zulip Johannes Hölzl (Nov 04 2018 at 21:19):

So it looks like everybody staying in the hotel will meet at 8:30 for breakfast and then we visit Johann

view this post on Zulip Michael Jendrusch (Nov 04 2018 at 21:45):

Can you just explain (to a pure mathematician) what biology has to do with symmetric monoidal categories? I last went to a biology class about 30 years ago by the way.

It's not really biology as much as it is microfluidics, where you can have some sample inlets or outlets (objects), together with ways to connect inlets with outlets, such as plain channels, mixers, etc., which do different things to the sample flowing through them (morphisms). Then you can "connect" the outlets of one microfluidic device to the inlets of of another (composition), or put two microfluidic devices next to each other (tensor product). The braiding is exchanging the order of two in- or outlets, which should satisfy the laws for a symmetric monoidal category. As you can flip the directionality of many microfluidic elements in a way that makes sense, you also get a dagger structure for many interesting subsets of what is possible with microfluidics.
Then you have a symmetric monoidal (dagger-) category which gives the syntax of the subset of microfluidics you're interested in and you can give semantics as a functor from that monoidal category to a more meaningful category, say a category of dynamical systems.
Also, there is this whole thing with interpreting biological processes as reaction networks, where you have some proteins and metabolites (objects), with reactions (morphisms) between them, where the outputs of some reactions may be the inputs of another (composition) and multiple reactions may happen in parallel (tensor product), and then you have some functors to give semantics to those reaction networks.

view this post on Zulip David Michael Roberts (Nov 04 2018 at 22:08):

To add more to @Michael Jendrusch 's comment, the work of John Baez and collaborators recently has been heavily focused on treating 'network theory' (in a very broad sense) using categories: http://math.ucr.edu/home/baez/networks/

view this post on Zulip Kenny Lau (Nov 04 2018 at 22:46):

I finally arrived to the hotel

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:46):

On the subject of the surprising appearances of category theory in "applied" fields; Fong and Spivak's new text "Seven sketches in compositionality" is quite amazing.

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:47):

As an example, one of its chapters is called "Electric circuits: Hypergraph categories and operads"

view this post on Zulip Cyril Cohen (Nov 05 2018 at 07:20):

Hallo, I'm at the breakfast

view this post on Zulip Kenny Lau (Nov 05 2018 at 07:21):

ich bin auch fertig

view this post on Zulip Mario Carneiro (Nov 05 2018 at 07:26):

I looked up use of "fertig" and it means "ready" and also "exhausted"... seems confusing

view this post on Zulip Johan Commelin (Nov 05 2018 at 07:41):

Lol, in this context it definitely means "I'm ready (to go)"

view this post on Zulip Kenny Lau (Nov 05 2018 at 08:33):

Johannes is now lecturing about how to review PR's (and potentially accept a few of them).

view this post on Zulip Mario Carneiro (Nov 05 2018 at 08:42):

vids plz

view this post on Zulip Kenny Lau (Nov 05 2018 at 08:42):

do you have skype?

view this post on Zulip Kenny Lau (Nov 05 2018 at 08:42):

I'm skyping Kevin Buzzard now

view this post on Zulip Kenny Lau (Nov 05 2018 at 08:43):

but I can also accommodate you

view this post on Zulip Mario Carneiro (Nov 05 2018 at 08:55):

ok, I am @di..gama, but if you have vid setup you should record instead so others can see it

view this post on Zulip Cyril Cohen (Nov 05 2018 at 09:10):

We are currently looking at https://t.co/K6iX1lo6z5

view this post on Zulip Sebastian Ullrich (Nov 05 2018 at 09:12):

:)

view this post on Zulip Mario Carneiro (Nov 05 2018 at 09:12):

lol, isn't this his presentation for lean together? spoilers...

view this post on Zulip Sebastian Ullrich (Nov 05 2018 at 09:20):

Eh, that one should probably have a slightly different focus (externals instead of internals) if I don't get lazy...

view this post on Zulip Scott Morrison (Nov 05 2018 at 10:37):

Just read the slides, @Sebastian Ullrich, looks fantastic! :-)

view this post on Zulip Keeley Hoek (Nov 05 2018 at 12:28):

I'M EXCITED
I think time will measure my excitement but I'm still excited!

view this post on Zulip Johan Commelin (Nov 05 2018 at 16:18):

I hereby officially declare the first day of this workshop to be a Great Success™.

view this post on Zulip Kenny Lau (Nov 05 2018 at 16:47):

2018-11-05-1.png

view this post on Zulip Kenny Lau (Nov 05 2018 at 16:47):

one merge every 3 minutes!

view this post on Zulip Johan Commelin (Nov 05 2018 at 17:13):

Just look at this: https://github.com/leanprover/mathlib/pulse/daily

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:18):

:bell: Don't forget to compile the latest mathlib tonight (-; Otherwise you'll have to be waiting the first hour tomorrow morning... your computers are all in for some serious learning of new stuff. :lol: :graduate:

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:25):

plus one of the 15 or so PRs that was merged had a bug, and now mathlib is broken

view this post on Zulip Mario Carneiro (Nov 05 2018 at 18:30):

*was broken

view this post on Zulip Kenny Lau (Nov 05 2018 at 20:01):

so do we have some goals to achieve?

view this post on Zulip Johan Commelin (Nov 05 2018 at 20:04):

[ ] Hilbert basis
[ ] Sheaves
[ ] Manifolds
[ ] Limits/colimts
[ ] Adjoint functors

view this post on Zulip Kevin Buzzard (Nov 05 2018 at 20:39):

Galois theory, algebraic closure, perfectoid spaces, existence of non-cyclic groups

view this post on Zulip Kenny Lau (Nov 05 2018 at 23:23):

even my trick of making a copy and ensuring little changes still can't make the compilation faster...

view this post on Zulip Mario Carneiro (Nov 06 2018 at 07:01):

I'm going to sleep now, but I've got something for you guys to puzzle over tomorrow: leanprover-community/pfilter is beginning work on generalizing filters to preorders. @Johannes Hölzl if you have any ideas for how all your lifting and monad stuff works when separating the two levels of sets out, I'd like to hear it. I have not figured out what the new version of join has to do with the old one (which has a different type - filter (filter A) becomes pfilter (set (pfilter A)) which is not obviously related to pfilter (pfilter A), which is something new).

view this post on Zulip Johan Commelin (Nov 06 2018 at 07:27):

Good morning and sleep tight!

view this post on Zulip Kenny Lau (Nov 07 2018 at 08:23):

@Johan Commelin veele dank voor de workshop, and thanks to everyone for teaching me German and French :p

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:31):

(why is nobody online?) @Johannes Hölzl asked me if a(b+c) = ab+ac for ideals, and I said no at the time, but I have since realized that it is actually true, and I have pushed my proof. In other news, German trains are nice to work in!

view this post on Zulip Kevin Buzzard (Nov 07 2018 at 09:34):

Yes, this is true. The thing that's basically never true for ideals is additive cancellation: I+J=I+K is a long way from J=K, e.g. (n)+(m)=(gcd(m,n)) in int, so (2)+(3)=(2)+(5)=(1).

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:35):

you guys need to be more productive!

view this post on Zulip Kevin Buzzard (Nov 07 2018 at 09:35):

Multiplicative cancellation is sometimes true, but only in the 1-dimensional case, e.g. integers of a number field or Dedekind domains more generally (e.g. PID's) or when the underlying ideal you're trying to cancel is locally free of rank 1 (e.g. principal when R is an integral domain)

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:36):

feel free to comment on the PR

view this post on Zulip Kevin Buzzard (Nov 07 2018 at 09:36):

us guys have got to prepare lectures, go to committee meetings, organise meetings with MSc and PhD students, run seminars, cook for our family etc etc. You have no idea how much work is involved in being a grown-up

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:36):

I mean, the people in the workshop

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:37):

I'm the only one leaving at 10, they're all staying there for a while longer!

view this post on Zulip Kevin Buzzard (Nov 07 2018 at 09:37):

They might have to do the same :-) Every night in Paris I had to leave with Patrick and spend the evening doing admin (organising interviews for a PhD studentship and dealing with emails etc)

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:39):

well they're already there, as they have already commented on my PR

view this post on Zulip Kenny Lau (Nov 07 2018 at 09:48):

see you guys in the next train (if there is wifi!)

view this post on Zulip Johan Commelin (Nov 07 2018 at 10:22):

We've been watching @Cyril Cohen give a demo of SSreflect. It looks really powerful. And the good news: in principal we can have this in Lean (4?) as well.

view this post on Zulip Scott Morrison (Nov 07 2018 at 10:24):

Oh, I would have liked to have seen that.

view this post on Zulip Kenny Lau (Nov 07 2018 at 10:59):

you should have come! :p

view this post on Zulip Tobias Grosser (Nov 07 2018 at 11:48):

Dear all, thank you so much for this interesting visit. I am very much looking forward to the next lean meeting!

view this post on Zulip Cyril Cohen (Nov 07 2018 at 11:56):

Thank you all very much for your warm welcone. And also for teaching me how to use lean. I am really interested in continuing my experiments and also coming to the next lean meeting.

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:28):

@Cyril Cohen w.r.t to param: The constructor types provided to add_inductive refer to the type using already the constant to be defined. So the name map would be just: bool -> const `bool uparams

view this post on Zulip Cyril Cohen (Nov 07 2018 at 12:33):

@Johannes Hölzl yes I figured that out and completed the translation.
Now, is there a way to assign the result of a run_cmd to a variable (in order to propagate the translation table around?)

view this post on Zulip Cyril Cohen (Nov 07 2018 at 12:34):

(and I pushed the result if you want to have a look)

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:34):

You can use attributes

view this post on Zulip Cyril Cohen (Nov 07 2018 at 12:35):

@Johannes Hölzl can you point me towards a tutorial, or a (documented) example?

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:35):

so attributes are named databases which associates a list of theorems (and optional data) to each attribute.

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:35):

first, they are defined in lean/library/init/meta/attribute.lean

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:37):

you set up a new attribute using:

@[user_attribute]
meta def mono_rules : user_attribute :=
{ name := `mono_rules,
  descr := "lemmas usable to prove monotonicity" }
attribute [mono_rules] add_le_add mul_le_mul_of_nonneg_right

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:38):

I guess you want to associated the paramtricity relation to the type using the attribute?!

view this post on Zulip Rob Lewis (Nov 07 2018 at 12:43):

I think it's even better to use cached attributes here, if I understand the situation right. I'll try to set it up in a few min.

view this post on Zulip Cyril Cohen (Nov 07 2018 at 12:59):

I want to replace a "current" consts map after each call to param2.inductive

view this post on Zulip Rob Lewis (Nov 07 2018 at 13:05):

Do you want param2.inductive to take consts as an argument, or generate the current map automatically?

view this post on Zulip Rob Lewis (Nov 07 2018 at 13:07):

Wait, this shouldn't matter. You won't be calling param2.inductive manually, right?

view this post on Zulip Rob Lewis (Nov 07 2018 at 13:13):

Just pushed something, is this roughly what you need? You'll probably want to change it a bit.

view this post on Zulip Cyril Cohen (Nov 07 2018 at 13:16):

@Rob Lewis I'll take a look and tell you.

view this post on Zulip Cyril Cohen (Nov 07 2018 at 13:17):

I just need to go through security first.

view this post on Zulip Cyril Cohen (Nov 07 2018 at 13:48):

@Rob Lewis I think I understand. Should I replace the argument consts of all my functions by parametricity_attr.get_cache?

view this post on Zulip Rob Lewis (Nov 07 2018 at 13:49):

Yep, but it might take a little refactoring, since parametricity_attr depends on some of those functions.

view this post on Zulip Jeremy Avigad (Nov 07 2018 at 14:47):

@Cyril Cohen Welcome to the dark side. We definitely want to steal all your mathcomp work on analysis, and it will be great to have your help.

view this post on Zulip Jeremy Avigad (Nov 07 2018 at 14:57):

(We can also steal ideas from his work on homology: https://perso.crans.org/cohen/papers/fpmods.pdf, https://perso.crans.org/cohen/papers/slides_fpmodules_marelle.pdf.)

view this post on Zulip Rob Lewis (Nov 07 2018 at 15:13):

@Johan Commelin Let me add to the expressions of thanks for hosting this! It was both fun and productive, a good combo.

view this post on Zulip Johan Commelin (Nov 07 2018 at 15:14):

Can I deduce from this that you caught your train and that it has wifi?

view this post on Zulip Patrick Massot (Nov 07 2018 at 15:15):

Yes !

view this post on Zulip Patrick Massot (Nov 07 2018 at 15:16):

And thank you very much for hosting this!

view this post on Zulip Patrick Massot (Nov 07 2018 at 15:21):

@Jeremy Avigad we already started porting https://github.com/math-comp/analysis/blob/master/landau.v

view this post on Zulip Johan Commelin (Nov 07 2018 at 15:56):

LUG_Freiburg_insights.png

view this post on Zulip Johan Commelin (Nov 07 2018 at 15:56):

That's GitHub's summary of our hackathon!

view this post on Zulip Johan Commelin (Nov 07 2018 at 18:45):

LUG Freiburg 2018 — Report
We had a Lean User Group in the mathematical institute of Universität Freiburg on November 5–7, 2018.
Participants: Cyril Cohen, Johan Commelin, Johannes Hölzl, Tobias Grosser, Micheal Jendrusch, Kenny Lau, Rob Lewis, Patrick Massot

Johannes gave an update of the development status of Lean 4. Cyril gave a demo of SSreflect.
There were 23 pull requests merged into mathlib (the main mathematical library of Lean) and 6 new pull requests were created. This resulted in 7594 lines added to mathlib and 3163 deletions, changing 100 files.
The topics of these changes include the definition of the perfect closure of a field and the Stone–Cech compactification of a topological space. The Hilbert basis theorem was proved, after a major refactoring of the theory of modules. Others have worked on monoidal categories, sites and sheaves, little-o calculus, transport of structure and improvement of automation tactics. These projects are not finished yet, but should be merged into mathlib in the future.
The participants agreed that the face-to-face collaboration will ease future digital collaboration and that the workshop gave a valuable boost to the development of formalized mathematics in Lean.

view this post on Zulip Johan Commelin (Nov 07 2018 at 18:45):

(If you have any feedback for this little report, please let me know.)

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 18:49):

(My report was PowerPoint karaoke using Sebastian's slides he presented at the end of his MSR internship )

view this post on Zulip Simon Cruanes (Nov 07 2018 at 18:54):

are the slides about Lean 4 online somewhere?

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 18:56):

yep: http://leanprover.github.io/presentations/20181012_MSR/

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 18:57):

there is also:http://leanprover.github.io/talks/LeanAtGalois.pdf

view this post on Zulip Simon Cruanes (Nov 07 2018 at 19:02):

thank you! :)

view this post on Zulip Patrick Massot (Nov 07 2018 at 21:01):

Thanks for the report Johan! Of course it must be emphasized that all those merged PR wouldn't haven't mergeable without first having be written before the meeting, and often by people not attending the meeting. And also I think Mario participated in the merge effort from Pittsburg. Nonetheless I agree this was a very successful meeting. Maybe it's worth pointing out to some of your readers that Cyril only installed Lean the day before the workshop, and is now writing both regular Lean and meta-programming. I think it's a huge success that this meeting was able to welcome such an expert Coq user to our Lean community.

view this post on Zulip Scott Morrison (Nov 07 2018 at 21:12):

I'm not sure who the audience of the report is, but I'd put the sentence about statistics at the end.

view this post on Zulip Scott Morrison (Nov 07 2018 at 21:14):

I think it's worth mentioning the (existence of) "remote" participants, too. It's fun to wake up in the morning and see progress on favourite things having happened overnight on the other side of the world. :-)

view this post on Zulip Scott Morrison (Nov 07 2018 at 21:15):

And I want to beg that future Lean meetings stream more. :-)

view this post on Zulip Kenny Lau (Nov 07 2018 at 22:13):

@Chris Hughes you should have come! :P

view this post on Zulip Kenny Lau (Nov 08 2018 at 02:06):

@Johannes Hölzl du hast noch ein ander PR :D

view this post on Zulip Kenny Lau (Nov 08 2018 at 02:11):

(@Mario Carneiro this means: you have yet another PR)

view this post on Zulip Johan Commelin (Nov 08 2018 at 04:16):

(@Mario Carneiro this means: you have yet another PR)

why the english?

view this post on Zulip Mario Carneiro (Nov 08 2018 at 04:17):

he has to translate because he doesn't realize that everyone here uses the same language: lean

view this post on Zulip Johan Commelin (Nov 08 2018 at 04:18):

Well, he should have translated to Portuguese right?

view this post on Zulip Mario Carneiro (Nov 08 2018 at 04:18):

don't encourage him

view this post on Zulip Johan Commelin (Nov 08 2018 at 07:45):

Ok, I've updated the report after your suggestions. I will send it to my supervisors.

view this post on Zulip Kenny Lau (Nov 08 2018 at 08:30):

merged!


Last updated: May 13 2021 at 22:15 UTC