Machine-Checked Mathematics

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.

All applications received by 2 April will receive full consideration and applicants will be informed on their admissibility soon after that.