Lean for PDEs, an ICARM & SLMath collaboration
A hands-on workshop on using the Lean proof assistant to formalize partial differential equations and contribute to the PDE section of the Mathlib library.
Computational proof assistants let us build global, digital libraries of mathematics where every theorem is fully verified by a computer. In this workshop, you'll get to explore this exciting new technology and the ideas behind it, with a special focus on formalizing partial differential equations (PDEs). The Lean mathematical library, Mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. The main goal of this workshop is to help you start tangible projects that will contribute to the PDE section of the Mathlib library.
Description
Hosted by the Simons Laufer Mathematical Sciences Institute (SLMath) and the Institute for Computer-Aided Reasoning in Mathematics (ICARM), with support from the U.S. National Science Foundation.
This intensive will feature interactive sessions led by Rémy Degenne (University of Lille) and Michael Rothgang (Universität Bonn) on Monday, Tuesday, and Thursday. They, along with other Lean experts, will be available for on-site consultations at SLMath the week of October 6-10, 2025 to help you with your projects.
Audience: SLMath members in residence and interested mathematicians, including graduate students and researchers in academia and industry.
Please note: Please bring your PC as this is a hands-on workshop. Some familiarity with Lean will be helpful. Lunch is available to order each day for on-site attendees.
Financial Support: Limited funding for in-person participation is available for early career mathematicians (including graduate students).
Workshop Schedule: Monday-Thursday*, October 6-7-9, 2025 from 2:00-4:30pm US Pacific Time each day. [What time is that for me?]
Download a PDF flyer to share with your colleagues or networks
