The Trace Formula Project

The idea

Trace formulas sit at the center of modern analytic number theory. The Petersson and Kuznetsov formulas, the Selberg trace formula, and their relative versions are the tools behind results on moments of L-functions, subconvexity, equidistribution, and non-vanishing.

Yet there is no single place to look them up. Each paper and each book fixes its own normalizations of the forms, the measures, the Bessel transforms, and the Kloosterman sums, and a formula copied from one source rarely matches a formula copied from another without a page of bookkeeping. Variants that are standard in the folklore, such as weighted versions, versions with a fixed level or nebentypus, or versions for half-integral weight, are often not written down anywhere at all.

The goal of this book is to be the source for all things trace formulas: every formula, in every common normalization and variation, stated precisely and proved completely, with the conversions between conventions made explicit. It is organized so that the subject is learned once and then generalized.

• Start with SL₂(ℤ). Volume 1 develops the whole theory for the full modular group, where every object can be written down concretely and every proof can be followed to the end.
• Then generalize. The later volumes carry the same formulas, in the same order and with the same conventions, to congruence subgroups with nebentypus, to half-integral weight, to quaternionic forms, and onward to other groups and other kinds of forms. A reader who knows Volume 1 should be able to read off the changes.
• Compare with automorphic representations. Each volume has a part in the classical language of automorphic forms, a part in the language of automorphic representations, and a dictionary part that lines the two up statement by statement, so each trace formula can be read in whichever style suits the problem.

The material is developed in three formats at once, all built from one source:

• A book. The natural-language text, written in LaTeX with complete arguments and consistent conventions, and built as a PDF.
• A website. The same manuscript presented alongside its Lean sources, with Read, Watch, Formalization, Compare, and Map views for every section.
• A video series. Chapter lectures on Screech Math, built from the same source as the text.

The series

Each volume treats one setting, and each has three parts: A, automorphic forms; B, automorphic representations; and C, the dictionary between them.

• Volume 1 · The modular group SL₂(ℤ)1a in draft
• Volume 2 · Congruence subgroups of SL₂(ℤ), including nebentypusPlanned
• Volume 3 · Half-integral weightPlanned
• Volume 4 · Quaternionic formsPlanned

Every theorem in the book is paired with a Lean formalization, and the Compare view on the website puts the prose statement and its formal counterpart side by side. The formalizations build with no admitted proofs, but machine verification is separate from checking that the formal statement says what the prose says. That correspondence is reviewed by hand, and the videos are part of that review. See the Lean page for more on why.

Status

Get in touch

Comments, corrections, and requests for topics are very welcome. Email me at steven.creech@rutgers.edu.

This material is based upon work supported by the National Science Foundation under Award No. DMS-2602321. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.