Workshop: Machine-Checked Mathematics, March 2-4

Stream: general

[Rob Lewis]

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, 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

[Anne Baanen]

If I registered back in November for the in-person edition, I should not have to re-register, right?

[Rob Lewis]

No need to re-register, you're still on the list :smile:

[Rob Lewis]

There are more details being finalized, but a draft schedule is up on the workshop website: https://lean-forward.github.io/lorentz-center-meeting/

If you're planning to attend, please do register on the Lorentz Center website!

[Eric Rodriguez]

Sorry for my naivete, but should I go as a (currently) non-academic? Does it cost me money?

[Rob Lewis]

It's free, and you're very welcome to attend!

[Kevin Buzzard]

As someone who was registered for the in person workshop do I need to re-register?

[Kevin Buzzard]

Can I plug it on Twitter or would you rather I didn't?

[Rob Lewis]

Rob Lewis said:

No need to re-register, you're still on the list :smile:

[Rob Lewis]

Thanks for offering the Twitter plug! I think it's better to keep the plugging for this event to the proof assistant Zulips/mailing lists. We're targeting people with some proof assistant experience this time.

[Ashley Blacquiere]

@Rob Lewis Was any of this workshop recorded? I've been checked out for a couple months and missed that it happened... The schedule looks interesting!

[Rob Lewis]

It was recorded, but I'm not sure how accessible the recordings are. They were emailed to registered participants only IIRC. I'll look into it