The local Gan–Gross–Prasad conjecture for general spin groups: a Lean blueprint

How to read this blueprint

This blueprint accompanies the Lean 4 formalization GSpinGGP (work in progress) of the dissertation [ 1 ] : S. Pease, The Local Gan–Gross–Prasad Conjecture for General Spin Groups, Rutgers University–Newark, 2026, doi:10.7282/t3-qb3s-s249. It is cited as “Thesis”, with the numbers of the printed dissertation. The proof adapts Beuzart-Plessis’s local trace formula for unitary groups [ 5 ] and the work of Waldspurger [ 26 ] and Luo [ 17 ] on special orthogonal groups.

Every node is a Lean declaration, and every statement is formalized. The main theorem (Theorem 60) is proved in Lean from three kinds of inputs: results whose Lean proof is still missing (sorry), results from the literature that are assumed (Lean axioms), and definitions. Results are attributed as follows.

  • Proved: the Lean proof of this step contains no sorry. It may still rely, through the results it uses, on unproved steps or on the literature.

  • Not yet proved: the Lean proof is sorry. Its proof paragraph gives the intended argument.

  • Assumed from the literature: a “Literature” environment, with an “Assumed from” line giving the source. These are Lean axioms; they have no proof paragraph, and are never proved in this project. Each is a published statement, specialized to the groups and fields used here, with the source’s hypotheses checked; results the sources prove only for other groups (unitary, special orthogonal, …) and that are adapted here are stated as theorems instead (proved, or left open with a proof sketch), and their proof paragraphs list the ingredients.

  • Definitions: real Lean definitions (never axiomatized).

Where a Lean statement deliberately differs from the dissertation, its node says so in one line.

Colours in the dependency graph.

Boxes are definitions, ellipses are results. A green border means the statement is formalized, which is the case for every node. The interior colour gives the status of the proof:

  • light green fill: proved (the Lean proof of this step has no sorry);

  • dark green fill: proved, and so is everything it depends on (no sorry and no literature assumption among its ancestors);

  • blue fill: not yet proved (sorry); the statement and everything it uses are formalized, so the proof is ready to be written;

  • no fill (white), with a label starting with LIT-: assumed from the literature (Lean axiom);

  • light green box: a definition.

Because every result on the path of the main theorem rests on literature assumptions, none of them is dark green: the dark green nodes are the self-contained results. The graph’s own legend uses the generic wording of the blueprint software (“ready to be formalized” for the blue fill).

Status

(November 2026). The project builds with 45 declarations containing sorry; the main theorem depends on 33 of them and on 11 of the 12 literature assumptions. Classical facts about quadratic forms (Witt cancellation and decomposition, Cartan–Dieudonné, the classification over \(p\)-adic fields) are proved from the Tau Ceti library; Hilbert’s Theorem 90 for \(\mathrm{GL}_m\) is proved from Mathlib. Only results stated verbatim in the literature (specialized to general spin groups, with the source’s hypotheses checked) are literature assumptions; where the dissertation adapts or combines published results, the statement is a theorem whose proof is not yet formalized, and its proof sketch names the exact ingredients. The 11 unproved statements not on its path are collected in Chapter 9. To see exactly what the main theorem rests on, run #print axioms GSpinGGP.local_ggp.