A Lean 4 library for formal linguistics across semantics, syntax, pragmatics, morphology, phonology, and processing.
Linglib is a community-maintained library of linguistic theory in Lean 4. It states definitions and results from the literature on shared foundations, so that work in one area can be cumulatively built on and compared against work in another.
Linglib is under active development. Finding the right foundational definitions is an iterative, trial-and-error process that requires extensive discussion within the community. Most of the code in the library was written with AI assistance and needs more extensive review. Please report problems on the issue tracker. Authors whose work appears here can ask for a correction or for its removal.
lake exe cache get # Get mathlib cache
lake buildLinglib pins a specific toolchain (currently Lean v4.35.0 / mathlib v4.35.0), so your project's lean-toolchain must match. Add to your lakefile.lean:
require linglib from git
"https://github.com/linglib-community/linglib" @ "v4.35.0"(Use @ "main" to track the latest development instead of the pinned release.)
Then import Linglib — or, more selectively, e.g. import Linglib.Pragmatics.RSA.Basic.
- Project site & API docs: linglib.io, with the bibliography.
- Contributing: see CONTRIBUTING.md.
The code is Apache 2.0 — see LICENSE. Imported datasets keep their own licences and citations, listed in Linglib/Data/README.md.