Scientific organisers
-
María Inés de Frutos Fernández , Universidad Autónoma de Madrid
-
Heather Macbeth , Fordham University
About:
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 has applications to teaching and communication of mathematics, and will soon be able to help in mathematical research.
The main objectives of this workshop are to develop the community of female mathematicians who are skilled users of proof assistants, and to build the connections of this community with researchers in the related area of computational algebra.
The workshop will be introductory and collaborative, with tutorials for beginners and proposed projects which participants can work on in groups, and with a focus on recognizing and using participants’ existing skills. Collaborations between students, early-career and senior researchers will be actively encouraged. The proof assistant Lean will be used for the tutorials, which will be complemented by more specialised lectures on topics like state-of-the-art formalisation projects or the use of formalisation in mathematics teaching.
Participation
No late applications and walk-in attendees will be accepted.
If you have any updates to inform ICMS after your submission, we kindly ask you not to submit twice but contact us by email.
Scam Warning
We are aware of a number of current scams targeting participants at ICMS workshops in relation to registration or accommodation bookings. If you are approached by a third party (e.g., travellerpoint.org, Conference Committee or Royal Visit) asking for booking or payment details, these scammers may telephone or email you and tell you that they are organising accommodation in Edinburgh for you on behalf of ICMS. please ignore.
Please note:
i) ICMS never uses third parties to do our administration for events: messages will come directly from ICMS staff;
ii) ICMS never asks participants for credit card or bank details;
iii) If you have any doubts about an email you receive, please get in touch with us.
Programme
MONDAY 27 MAY 2024 | ||
Registration | ||
Welcome & intro | ||
Heather Macbeth, Fordham University | Lean Basics | |
Coffee Break | ||
Amelia Livingston, King's College London | Logic | |
Lunch | ||
María Inés de Frutos Fernández, Universidad Autónoma de Madrid | Projects presentation | |
Coffee Break | ||
Practice | ||
Welcome reception, hosted at ICMS | ||
TUESDAY 28 MAY 2024 | ||
Anne Baanen, Vrije Universiteit Amsterdam | Structures and Classes | |
Coffee Break | ||
Practice | ||
Lunch | ||
Heather Macbeth, Fordham University | Advanced Tactics | |
Coffee Break | ||
Chelsea Edmonds, University of Sheffield | Research talk: An Introduction to Isabelle for Formalised Mathematics | |
Practice | ||
WEDNESDAY 29 MAY 2024 | ||
María Inés de Frutos Fernández, Universidad Autónoma de Madrid | Algebra and Number Theory | |
Coffee Break | ||
Practice | ||
Lunch & free afternoon | ||
THURSDAY 30 MAY 2024 | ||
Kim Morrison, Lean Focused Research Organization | Category Theory | |
Coffee Break | ||
Practice | ||
Lunch | ||
Jennifer Balakrishnan, Boston University | Research talk: Point-counting on curves, p-adics, and applications | |
Coffee Break | ||
Panel: Teaching (with) Lean | ||
Practice | ||
Workshop dinner | ||
FRIDAY 31 MAY 2024 | ||
Maryna Viazovska, EPFL | Research talk: On a path to formalizing sphere packing in dimension 8 | |
Coffee Break | ||
María Inés de Frutos Fernández, Universidad Autónoma de Madrid | Returns on projects | |
Lunch & end of the workshop |