In the last few years, there has been a rapid growth in the community of mathematicians using proof assistants to formalise mathematical results. Besides verifying the correctness of theorems beyond any reasonable doubt, formalisation had applications to teaching and communication of mathematics, and would soon be able to help in mathematical research. 

The main objectives of this workshop were to develop the community of female mathematicians who were skilled users of proof assistants, and built the connections of this community with researchers in the related area of computational algebra.

The workshop was introductory and collaborative, with tutorials for beginners and proposed projects which participants could work on in groups, and with a focus on recognizing and using participants’ existing skills. Collaborations between students, early-career and senior researchers would be actively encouraged. The proof assistant Lean used for the tutorials, which would be complemented by more specialised lectures on topics like state-of-the-art formalisation projects or the use of formalisation in mathematics teaching.