Participant Testimonials

May 21 - May 26, 2023

Very productive and friendly workshop! The Juniper Hotel was a good location for focused work and interaction. I think the participants all learned a lot and came away with new plans and ideas for expanding the reach of Lean's mathematics library and mathematical formalization more generally.

Jake Levinson Mathematics, Simon Fraser University

This workshop surprised me by demonstrating just how many cohomology theories are within the range of formalization. As the week progressed, I came to understand that this is due in large part to the extensive development of category theory and homological algebra in Lean's Mathlib library. This new perspective on what is possible will certainly influence the direction of my future work. I also found it valuable and very pleasant to meet several collaborators for the first time.

Oliver Nash Imperial College London

Great atmosphere and successful workshop, that was instructive, useful and brought up new questions and possible answers.

Filippo A. E. Nuccio Mortarino Majno di Capriglio Maître de Conférences
Mathematics, Univ Lyon, UJM Saint-Étienne

The BIRS workshop was very stimulating for me. I learned a lot and made new scientific connections, both on the formalization side and on the theory side of things. Being together in the beautiful surroundings of Banff with a relatively small group of experts was very helpful for this. Working in small groups of varying composition, we produced a number of contributions to Lean's mathematical libraries, and I hope that some of the scientific discussions that I had at BIRS will lead to new collaborations in the future.

Sam van Gool Maître de conférences
IRIF, Université Paris Cité

As a tenured faculty member who has some familiarity with proof assistants but little experience with Lean, this workshop was fantastic! The organizational structure was great for productivity--a handful of interesting talks throughout the day, with plenty of time in-between to work collaboratively. As a newcomer, I am grateful for the opportunity to give a talk on my goals in entering the mathematical Lean community, which led to, with the help of experts and colleagues, the formalization of local cohomology, a commutative-algebraic notion introduced by Grothendieck. I cannot overstate how much I learned during the workshop about formalization of mathematics in Lean and the state of the math library, through interactions with the welcoming (and patient) organizers and experienced workshop participants.

Emily Witt Associate Professor
Mathematics, University of Kansas