A Lean 4 library for formal linguistics across semantics, syntax, pragmatics, morphology, phonology, and processing.