smoothness Writing and formalizations around manifolds, algebras, and their various categories and toposes. Formalizations are in Lean for now.