Participant Testimonials
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.
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.
Great atmosphere and successful workshop, that was instructive, useful and brought up new questions and possible answers.
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.
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.
Mathematics, University of Kansas
