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
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.
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.
Register was possible on the Lorentz Center website but has closed.
All times in CET; subject to change.
| 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 |
| 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 |
| 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) |