International Conference
Education
, London Borough of Brent, United Kingdom
2026-07-07 - 2026-07-18
info@icarm.io
Conference Details : Computational proof assistants now make it possible to develop global, digital mathematical libraries with theorems that are fully checked by computer. This summer school will introduce students to the new technology and to the goals and benefits of formalized mathematics, including metaprogramming and autoformalization. Students will learn to use the Lean interactive proof assistant, and by the end of the session, they will be in a position to formalize mathematics on their own, join the Lean community, and contribute to its mathematical library.
