Zulip Chat Archive

Stream: general

Topic: LUG Freiburg 2018

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

Patrick Massot (Sep 11 2018 at 07:28):

@Johan Commelin I'll come

Johannes Hölzl (Sep 11 2018 at 08:49):

@Johan Commelin I'll come too

Kenny Lau (Sep 11 2018 at 14:36):

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

Kenny Lau (Sep 11 2018 at 14:37):

@Kevin Buzzard how does this work?

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.

Kenny Lau (Sep 11 2018 at 14:56):

I see

Cyril Cohen (Sep 13 2018 at 14:19):

@Johan Commelin I am interested in coming.

Johan Commelin (Sep 13 2018 at 14:26):

Cool! I'm looking forward to meeting you.

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.

Johan Commelin (Sep 14 2018 at 09:18):

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

Johan Commelin (Sep 14 2018 at 09:19):

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

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.

Tobias Grosser (Sep 14 2018 at 10:51):

Seems things could work out.

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

Tobias Grosser (Sep 14 2018 at 11:50):

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

Johan Commelin (Sep 14 2018 at 11:54):

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

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.

Johannes Hölzl (Sep 18 2018 at 08:54):

I got the mail

Cyril Cohen (Sep 18 2018 at 09:09):

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

Johan Commelin (Sep 18 2018 at 09:09):

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

Johan Commelin (Sep 18 2018 at 09:09):

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

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)

Rob Lewis (Sep 18 2018 at 09:53):

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

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

Patrick Massot (Sep 19 2018 at 12:43):

@Johan Commelin

Johan Commelin (Sep 19 2018 at 13:07):

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

Patrick Massot (Sep 19 2018 at 13:08):

To which email address?

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

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

Cyril Cohen (Sep 24 2018 at 15:51):

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

Patrick Massot (Sep 24 2018 at 17:32):

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

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:

Kenny Lau (Oct 03 2018 at 22:23):

what are the starting/ending times?

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.

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.

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.

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?

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

Johan Commelin (Oct 23 2018 at 13:57):

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

Tobias Grosser (Oct 23 2018 at 17:18):

I will be around 16:00 in Freiburg.

Tobias Grosser (Oct 23 2018 at 17:18):

Would be great to meet for dinner.

Tobias Grosser (Oct 23 2018 at 17:19):

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

Tobias Grosser (Oct 23 2018 at 17:20):

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

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.

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.

Johan Commelin (Oct 31 2018 at 18:20):

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

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

Kenny Lau (Nov 03 2018 at 22:40):

Should we meet on Sunday as well?

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.

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?

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.

Tobias Grosser (Nov 04 2018 at 12:10):

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

Kenny Lau (Nov 04 2018 at 12:46):

I might arrive on monday

Tobias Grosser (Nov 04 2018 at 13:06):

@Kenny Lau, is this last-minute booking?

Kenny Lau (Nov 04 2018 at 13:38):

mostly

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.

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?

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.

Patrick Massot (Nov 04 2018 at 15:10):

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

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

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.

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.

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.

Patrick Massot (Nov 04 2018 at 20:41):

I love hotels having eduroam wifi!

Patrick Massot (Nov 04 2018 at 20:42):

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

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

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

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.

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/

Kenny Lau (Nov 04 2018 at 22:46):

I finally arrived to the hotel

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.

Scott Morrison (Nov 04 2018 at 23:47):

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

Cyril Cohen (Nov 05 2018 at 07:20):

Hallo, I'm at the breakfast

Kenny Lau (Nov 05 2018 at 07:21):

ich bin auch fertig

Mario Carneiro (Nov 05 2018 at 07:26):

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

Johan Commelin (Nov 05 2018 at 07:41):

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

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

Mario Carneiro (Nov 05 2018 at 08:42):

vids plz

Kenny Lau (Nov 05 2018 at 08:42):

do you have skype?

Kenny Lau (Nov 05 2018 at 08:42):

I'm skyping Kevin Buzzard now

Kenny Lau (Nov 05 2018 at 08:43):

but I can also accommodate you

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

Cyril Cohen (Nov 05 2018 at 09:10):

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

Sebastian Ullrich (Nov 05 2018 at 09:12):

Mario Carneiro (Nov 05 2018 at 09:12):

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

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

Scott Morrison (Nov 05 2018 at 10:37):

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

Keeley Hoek (Nov 05 2018 at 12:28):

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

Johan Commelin (Nov 05 2018 at 16:18):

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

Kenny Lau (Nov 05 2018 at 16:47):

2018-11-05-1.png

Kenny Lau (Nov 05 2018 at 16:47):

one merge every 3 minutes!

Johan Commelin (Nov 05 2018 at 17:13):

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

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:

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

Mario Carneiro (Nov 05 2018 at 18:30):

*was broken

Kenny Lau (Nov 05 2018 at 20:01):

so do we have some goals to achieve?

Johan Commelin (Nov 05 2018 at 20:04):

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

Kevin Buzzard (Nov 05 2018 at 20:39):

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

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

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

Johan Commelin (Nov 06 2018 at 07:27):

Good morning and sleep tight!

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

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!

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

Kenny Lau (Nov 07 2018 at 09:35):

you guys need to be more productive!

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)

Kenny Lau (Nov 07 2018 at 09:36):

feel free to comment on the PR

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

Kenny Lau (Nov 07 2018 at 09:36):

I mean, the people in the workshop

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!

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)

Kenny Lau (Nov 07 2018 at 09:39):

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

Kenny Lau (Nov 07 2018 at 09:48):

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

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.

Scott Morrison (Nov 07 2018 at 10:24):

Oh, I would have liked to have seen that.

Kenny Lau (Nov 07 2018 at 10:59):

you should have come! :p

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!

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.

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

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

Cyril Cohen (Nov 07 2018 at 12:34):

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

Johannes Hölzl (Nov 07 2018 at 12:34):

You can use attributes

Cyril Cohen (Nov 07 2018 at 12:35):

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

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.

Johannes Hölzl (Nov 07 2018 at 12:35):

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

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

Johannes Hölzl (Nov 07 2018 at 12:38):

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

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.

Cyril Cohen (Nov 07 2018 at 12:59):

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

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?

Rob Lewis (Nov 07 2018 at 13:07):

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

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.

Cyril Cohen (Nov 07 2018 at 13:16):

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

Cyril Cohen (Nov 07 2018 at 13:17):

I just need to go through security first.

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?

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.

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.

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

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.

Johan Commelin (Nov 07 2018 at 15:14):

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

Patrick Massot (Nov 07 2018 at 15:15):

Yes !

Patrick Massot (Nov 07 2018 at 15:16):

And thank you very much for hosting this!

Patrick Massot (Nov 07 2018 at 15:21):

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

Johan Commelin (Nov 07 2018 at 15:56):

LUG_Freiburg_insights.png

Johan Commelin (Nov 07 2018 at 15:56):

That's GitHub's summary of our hackathon!

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.

Johan Commelin (Nov 07 2018 at 18:45):

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

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 )

Simon Cruanes (Nov 07 2018 at 18:54):

are the slides about Lean 4 online somewhere?

Johannes Hölzl (Nov 07 2018 at 18:56):

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

Johannes Hölzl (Nov 07 2018 at 18:57):

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

Simon Cruanes (Nov 07 2018 at 19:02):

thank you! :)

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.

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.

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