p-adic modular forms in Lean — Formalization of the basic theory of p-adic modular forms for GL₂/Q following Serre’s approach, where a p-adic modular form is a power series in Q_p⟦q⟧ arising as the coefficientwise limit of a sequence of classical modular forms. The main goals include the definition of p-adic modular forms via q-expansions, the construction of the weight space, families of Eisenstein series, the p-adic zeta function, and the algebraic prerequisites for Hecke operators, Λ-adic modular forms, and Hida theory. The project contributes reusable arithmetic infrastructure to mathlib.
p-adic analysis — Development of basic nonarchimedean functional analysis in Lean, with a focus on p-adic Banach and Fréchet spaces. The goal is to enrich mathlib with a solid and reusable body of p-adic analysis that can support later work in arithmetic geometry and number theory, including p-adic modular forms, Galois representations, and the broader framework of the p-adic Langlands program.