IRC channel on https://libera.chat

Stream: general

[Calvin Lee]

Just a quick heads up that I've registered the #lean channel on https://libera.chat. Libera is a bastion of the free software community and has many programming language channels (including a small group of type theorists and category theorists whom I talk to often) and I thought it appropriate to have a small lean presence there as well.

This definitely isn't meant to be a replacement for the Zulip in any way, but rather a small area for lighthearted discussion, which can send people to the zulip for discussion that should happen there.

If you enjoy idling in IRC please stop by :grinning_face_with_smiling_eyes: