All of the projects here are only the .lean files and only depend on Mathlib.
Various small formalizations in the lean proof assistant