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.