Zulip Chat Archive

Stream: FoMM / Lean Together 2020

Topic: Lean Together


view this post on Zulip Rob Lewis (Dec 28 2019 at 20:53):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 19:11):

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

view this post on Zulip Rob Lewis (Jan 14 2020 at 19:14):

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

view this post on Zulip Rob Lewis (Jan 14 2020 at 19:15):

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

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 19:16):

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

view this post on Zulip Reid Barton (Jan 14 2020 at 19:17):

Diaeresis (which I apparently can't spell)

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 19:18):

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

view this post on Zulip Sebastian Ullrich (Jan 14 2020 at 19:29):

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

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 19:31):

ha ha I added it.

view this post on Zulip Patrick Massot (Jan 14 2020 at 20:53):

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

view this post on Zulip Sebastien Gouezel (Jan 14 2020 at 20:54):

Also, it's Sylvie, not Silvie.

view this post on Zulip Kevin Buzzard (Jan 14 2020 at 21:03):

Also, it's Sylvie, not Silvie.

Many thanks! Fixed in master.

view this post on Zulip Jeremy Avigad (Jan 15 2020 at 13:10):

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


Last updated: May 18 2021 at 09:14 UTC