Lean Together

Stream: FoMM / Lean Together 2020

[Rob Lewis]

The last couple days are devoted to Lean/mathlib topics. We have a handful of talks planned, but also some open blocks of time for discussion, planning, etc. There are a few things on the lineup already: we should talk about and coordinate peoples' ongoing projects, discuss moving mathlib to 3.5c, speculate about Lean 4, etc. But please think about other topics you'd like to bring up. If you let us know here in advance, we can add them to the official plan.

[Kevin Buzzard]

I wrote a blog post about the meeting: https://xenaproject.wordpress.com/2020/01/14/lean-together-2020/

[Rob Lewis]

Why does @Sebastien Gouezel get an umlaut but @Johannes Hölzl doesn't? :stuck_out_tongue_wink:

[Rob Lewis]

(The opposite of their Zulip names, apparently...)

[Kevin Buzzard]

I believe that in German it's legitimate to replace the o-umlaut with an oe, but I don't think there's any such trick you can do in French. I just didn't know how to typeset an o umlaut but I copied the non-umlaut (umlaut's can't go on an e, it's something else I think?) from Gouezel's web pages ;-)

[Reid Barton]

Diaeresis (which I apparently can't spell)

[Kevin Buzzard]

yeah that, I didn't know how to spell it ;-) I've added the umlaute.

[Sebastian Ullrich]

@Kevin Buzzard You forgot fixing the most famous of them all, Mjölnir!

[Kevin Buzzard]

ha ha I added it.

[Patrick Massot]

There is no umlaut in French, Sébastien has a tréma. See https://en.wikipedia.org/wiki/Diaeresis_(diacritic)

[Sebastien Gouezel]

Also, it's Sylvie, not Silvie.

[Kevin Buzzard]

Also, it's Sylvie, not Silvie.

Many thanks! Fixed in master.

[Jeremy Avigad]

@Kevin Buzzard Thanks for the lovely blog post! It is a nice description of the meeting, and gratifying to read.