Sander Dahmen, Rob Lewis, 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, so check back soon for an updated program! The event is still officially happening through the Lorentz Center, so if you’re interested, please register at https://www.lorentzcenter.nl/machine-checked-mathematics.html