MSRI/SLMath's Summer Research in Mathematics program provides space, funding, and the opportunity for in-person collaboration to small groups of mathematicians, especially women and gender-expansive individuals, whose ongoing research may have been disproportionately affected by various obstacles including family obligations, professional isolation, or access to funding. Through this effort, MSRI/SLMath aims to mitigate the obstacles faced by these groups, improve the odds of research project completion, and deepen their research experience. The ultimate goal of this program is to enhance the mathematical sciences as a whole by positively affecting the research and careers of all of its participants and assisting their efforts to maintain involvement in the research community.

The ultimate goal of this program is to enhance the mathematical sciences as a whole by positively affecting the research and careers of all of its participants and assisting their efforts to maintain involvement in the research community.

Some basic concepts in mathlib and the dependencies between them

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 the ideas behind it, and will encourage them to think about the goals and benefits of formalized mathematics. 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.