Machine-Checked Mathematics

We held an online workshop in March 2022. This website concerns the onsite workshop in July 2023.

This workshop aims to introduce interested mathematicians to the theory and practice of proof assistants, and to spur collaboration between such mathematicians and current proof assistant users.

The workshop targets mathematicians who have heard about the technology from recent publicity pushes but who have not yet tried to use a proof assistant themselves, as well as more experienced proof assistant users interested in new mathematical applications. There will be a blend of tutorials and plenary lectures, with hands-on sessions of the Lean proof assistant where novices will work on formalization projects alongside experts.

Check out this blog post for a workshop experience, including more info on the formalization projects.