Work in progress

The local Gan–Gross–Prasad conjecture for general spin groups, in Lean

A Lean 4 + Mathlib formalization of the dissertation of Samantha Pease (Rutgers University–Newark, 2026, doi:10.7282/t3-qb3s-s249).

The main theorem is stated and its proof assembled in Lean, but it still rests on unproved steps and on results from the literature assumed as axioms. The blueprint shows which.

Dependency graph Every definition, theorem and assumed result, coloured by formalization status. Blueprint The argument, statement by statement, linked to the Lean declarations. Blueprint (PDF) The same, as a printable document. Source on GitHub The Lean code, with build instructions and current status.