Stream: General

Topic: Workshop: Machine-Checked Mathematics

view this post on Zulip Rob Lewis (Feb 18 2022 at 16:00):

Hi Isabelle users! I've been trying to send this announcement to the mailing list, but it seems like my attempts aren't going through. If anyone is able to forward the message to the list (or approve mine, if it's stuck in a queue), I'd really appreciate it.

Sander Dahmen, Assia Mahboubi, and I have been planning a workshop for a while at the Lorentz Center in Leiden. Pandemic planning is impossible and the workshop keeps changing shape. But we can finally be certain enough to announce: we will be hosting a virtual workshop, Machine-Checked Mathematics, March 2-4! It will happen European afternoons, in an attempt to be accessible by as many people as possible.

Our workshop is organized around the idea of a “library showcase.” Proof assistant users from different communities will introduce the audience to some definition, design decision, abstraction, tool, or other feature of their library that is particularly good at serving some purpose. These showcases will be demo-style, with plenty of time for questions and discussion. We strongly encourage interacting with the presenters during these demos.

The goal of these showcases is not for people to describe an entire library or present a formal paper. The formalized mathematics community is small and fragmented into even smaller communities by prover choice. We want to spur discussion of how good ideas can be adopted or adapted across community boundaries.

We're still confirming and scheduling speakers. A preliminary schedule is on our website:
The event is officially happening through the Lorentz Center, so if you're interested, please register as soon as possible at

Hope to see many of you there!
-Rob (and Sander and Assia)

view this post on Zulip Kevin Kappelmann (Feb 18 2022 at 21:30):

Hi Rob, did you use or ?
Cambridge uni changed their email server a while ago and since then multiple people have reported similar issues. Maybe one of the aliases broke during the migration. If that does not help either, I can forward the email.

view this post on Zulip Rob Lewis (Feb 18 2022 at 22:35):

I actually tried both -- cl-isabelle-users first, and earlier today when someone pointed out my first didn't go through

view this post on Zulip Kevin Kappelmann (Feb 20 2022 at 13:04):

Okay, I just forwarded it!

Last updated: Aug 15 2022 at 02:13 UTC