Hello, everyone! My name is Jana Göken, a master's student in mathematics from Bremen. Today, I want to share with you my experiences at the Machine-Checked Mathematics workshop that introduced me to the world of proof assistants, specifically Lean. The workshop took place in Leiden from July 10th to July 14th 2023, and it was an amazing and educational journey.

My First Encounter with Lean

The first time I heard about the proof assistant Lean, or any proof assistant, was in the summer of 2022 when I attended the International Congress of Mathematicians for Number Theory and Algebraic Geometry in Zürich. There, I took the opportunity to attend a fascinating talk by Kevin Buzzard about the proof assistant Lean. I was instantly intrigued because, with the current rise of AI, I saw the great potential in the idea of using Lean to aid in mathematical proofs. Despite the excitement, I wasn't sure whether I would be able to start my own journey with Lean by myself.

Fast forward to May 2023, and I received an email from "Women in Number Theory" about an upcoming workshop in Leiden focused on learning the Lean proof assistant. This was the perfect opportunity for me! Excited about the prospect of learning Lean, I immediately signed up.

Inclusive Community

For me, the best aspect of this workshop was definitely the welcoming environment. I got to know really kind and amazing people. As a woman in the field of mathematics, I felt incredibly welcome, and I got the impression that everyone felt very welcome, regardless of gender, sexuality, or appearance. Consequently, we were a colorful bunch of people with diverse styles and backgrounds, and I really enjoyed the variety.

Diving into Lean

The workshop spanned five days, from July 10th to July 14th, at the Lorentz Center in Leiden. The participants received detailed instructions to download Lean and the mathlib library a few days before the workshop. Previous worries whether I, as a complete beginner in Lean, could follow the workshop, were quickly put to rest by reassuring emails, a really supportive environment, and kind experts who were answering every question. For those of us who faced challenges during the installation process, there was a timeslot on the first day to fix any problems and ensure that everyone was ready to begin.

Each day of the workshop was filled with a variety of activities, including talks, guided tutorials, exercise sessions, and group projects. It was incredible to witness our progress throughout the week. On the first day, we struggled with seemingly simple proofs, like associativity of addition. But by the last day, everyone was presenting their unique projects building on the mathlib library, something I never thought possible at the beginning.

One of the most valuable takeaways from the workshop was learning about the Zulip platform, where the Lean community actively communicates. Even after the workshop concluded, we could easily connect with the experts, ask questions, and seek guidance as we continued our projects.

Projects

The highlight of the workshop was undoubtedly the group projects. On the initial day of the workshop, everyone convened to brainstorm project concepts—ideas that had not yet been formalized in Lean but showcased promise for a week-long development journey. Subsequently, participants formed project groups, ensuring a mix of experienced Lean users and newcomers within each group. Engaging in a hands-on Lean project was both enjoyable and enlightening, with daily progress adding to the experience. In this way, a range of captivating and ambitious projects were undertaken by all workshop attendees:

• Recurrence and Minimality on Metric Spaces by Guillaume Dubach, Sébastien Goüezel, Marco Lenci, and Marcello Seri
• The Hasse-Minkowski Theorem by Alex Best, Kevin Buzzard, Marco Streng, Hanneke Wiersema, and Rosa Winter
• Octonions by Filippo Nuccio, and Matthieu Piquerez
• Formally Real Fields by Mahoor Alavioun, Riccardo Brasca, Maryam Emamjomeh Zadeh, Ignasi Sánchez Rodríguez, and Florent Schaffhauser
• The Cyclotomic Character by Jennifer Balakrishnan, Alex Best, Kevin Buzzard, Marco Streng, Hanneke Wiersema, and Rosa Winter
• Computing the Reduced Row Echelon Form Mohanad Ahmed, Anne Baanen, Sudhir Murthy, and Wessel de Weijer
• Fuchsian Groups by Jana Göken, Bhavik Mehta, and Oliver Nash
• Skew Polynomial rings and Drinfeld modules by María Inés de Frutos Fernández, Carlos Caralps, Xavier Généreux, Benoît Guillemet, and Nandagopal Ramachandran
• Properties of scheme morphisms by Amelia Livingston, Wim Nijgh, Torger Olson, and Jonas van der Schaaf
• Goppa codes by D. J. Bernstein
• Moebius sum, Brouckner-Wallis algorithm by Sam van Gool, and Harald Helfgott
• Resultants by Sander Dahmen, Dimitrios Mitsios, and Qizheng Yin
• Sturm polynomials by Antoine Chambert-Loir, and Cyril Cohen

The interested reader can find short project summaries here.

Exciting Future for Mathematics

In conclusion, my experience at the Lean workshop in Leiden was amazing. I met wonderful people, explored new mathematical territories, and gained valuable skills that will undoubtedly shape the future of my mathematical journey. I wholeheartedly recommend anyone interested in proof assistants, particularly Lean, to attend such workshops. The education and sense of community you will discover are truly remarkable.

I am very grateful for this amazing opportunity, and I hope to see everyone again soon, collaborating and making significant contributions to mathematics using Lean. With proof assistants like Lean paving the way, I am confident that artificial intelligence will play a vital role in the future of mathematics.

If you're curious about the capability of Lean, don't hesitate to dive in and discover the power of proof assistants for yourself.