Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Workshop: Machine-Checked Mathematics


view this post on Zulip Email Gateway (Feb 20 2022 at 13:04):

From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Hi all,

Rob Lewis (CC) has been trying to send below announcement to the mailing
list, but it seems like his attempts aren't going through. So I offered
to forward it on his behalf:


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: https://lean-forward.github.io/lorentz-center-meeting/
The event is officially happening through the Lorentz Center, so if
you're interested, please register as soon as possible at
https://www.lorentzcenter.nl/machine-checked-mathematics.html

Hope to see many of you there!

-Rob (and Sander and Assia)


Last updated: Jul 15 2022 at 23:21 UTC