Machine-Checked Mathematics A meeting for mathematical formalizers

This website hosts information for the workshop Machine-Checked Mathematics, hosted virtually by the Lorentz Center March 2-4, 2022.

Organizers: Sander Dahmen, Robert Y. Lewis, Assia Mahboubi

Workshop ogranization

For pandemic-related reasons, this workshop has changed dates and formats a number of times. We are excited for a lively, casual, friendly gathering of mathematical formalizers.

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.

John Harrison will give a keynote talk at the end of the workshop.

Coordinates

The workshop will be held on Zoom.
We encourage longer text discussions related to the workshop to be held on Zulip instead of Zoom chat. This way they will not be lost when the Zoom meeting ends. We will use a platform for social interaction before and after the sessions and during coffee breaks.

Registered users should have received links to all of these venues by email. Please contact the organizers directly if you did not.

The workshop will happen 2:30pm-6:00pm CET, in an attempt to be accessible to as many time zones as possible.

Registration

Register was possible on the Lorentz Center website but has closed.

Schedule

All times in CET; subject to change.

Wednesday, March 2:

Time Speaker Topic
2:30pm Sander Dahmen, Assia Mahboubi, Robert Y. Lewis Welcome/introduction
2:45pm Manuel Eberl The Mathematical Libraries of Isabelle/HOL
3:30pm   Coffee break
3:45pm Cyril Cohen Summation of functions on a finite support (Coq)
4:15pm Yury Kudryashov Many kinds of integrals (Lean)
4:45pm   Coffee break
5:00pm Mario Carneiro Lessons from Metamath
5:30pm John Harrison The HOL Light mathematical libraries

Thursday, March 3:

Time Speaker Topic
2:30pm Sébastien Gouëzel Topology with and without typeclasses (Lean)
3:00pm Guillaume Melquiond Verified bounds on mathematical functions (Coq)
3:30pm   Coffee break
3:45pm Freek Wiedijk Mizar: the language, the system, the library
4:15pm Frédéric Dupuis and Heather Macbeth Semilinear maps (Lean)
4:45pm   Coffee break
5:00pm Adam Naumowicz Library integrity and redundancy (Mizar)
5:30pm   Discussion time

Friday, March 4:

Time Speaker Topic
2:30pm Bohua Zhan Design of user interfaces for proofs and computation (HolPy)
3:00pm Anne Baanen Type classes for morphisms and substructures (Lean)
3:30pm   Coffee break
3:45pm Kevin Buzzard, Angeliki Koutsoukou-Argyraki, Yiannos Stathopoulos, and Laurent Thery Discussion/demos: theorem search and discovery
4:15pm   Plenary discussion
4:45pm   Coffee break
5:00pm John Harrison Automated and interactive theorem proving: a historical perspective (Keynote)

Confirmed speakers