Machine-Checked Mathematics: an Introduction to Formally Verified Mathematics

This school aims at introducing interested mathematicians to the theory and practice of interactive theorem provers, such as Lean or Rocq (previously named Coq) and to spur collaboration between such mathematicians and current proof assistant expert users. This school targets participants with diverse backgrounds in mathematics, but without a specific knowledge in logic or program verification. The expected audience consists of curious mathematicians who have heard about the technology from recent publicity pushes (such as Peter Scholze's Liquid Tensor experiment, the verification of the Kepler Conjecture in discrete geometry, of the Odd Order theorem in finite group theory. etc.) but who have not yet tried to use a proof assistant themselves. A special emphasis will be put on the verification of computational mathematics, typically computer algebra. The event will consist of a blend of tutorials and plenary lectures, with hands- on sessions where novices will work on formalization projects alongside experts.