The mathematical library for Lean — a large, community-maintained collection of formalized mathematical theorems that allows new formalization to build on verified foundations. The existence of Mathlib is what made formalizing the physics paper practical; no equivalent existed for physics until PhysLib
