$p$-adic Representation Theory
Formalization of $p$-adic Representation Theory in Lean4
Our ultimate goal is to formalize $p$-adic Representation Theory in Lean. Currently, we focus on smooth $\mathbb{C}$-representation theory of $G(K)$, where $G$ is a split reductive group and $K$ is a NA local field.
The blueprint and homepage of this project relies on the Lean blueprint tool by Patrick Massot.
The project webpage contains the blueprint and dependency graph.