Workshop

The formalization of mathematics is undergoing a quiet revolution. Computational proof assistants like Lean now make it possible to build verified, machine-checkable libraries of mathematics at scale, and the frontier of partial differential equations (PDEs) stands as one of the most profound and underexplored territories in this landscape. At the same time, large language models and AI for mathematics (AI4Math) are beginning to reshape how researchers discover, conjecture, and verify mathematical results. This workshop brings together three communities, PDE analysts, Lean/Mathlib developers, and AI/AI4Math researchers from both academia and industry, to chart a shared path forward. Our central aim is to produce a clear, community-endorsed roadmap (1-year, 3-year, and 5-year horizons) for the formalization and AI-assisted analysis of PDEs, spanning undergraduate and graduate textbook material through to active research frontiers. We will identify the PDE topics most ripe for formalization in Mathlib, the AI tools best positioned to accelerate that work, and the collaborative structures needed to sustain long-term progress. Audience: SLMath members in residence and interested mathematicians, Lean/mathlib enthusiasts, AI researchers, including graduate students and researchers in academia and industry. Please note: You may consider bringing your PC as this event might involve hands-on coding sessions, but this is not required. 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).