A proof of the sharpness conjectures for all saturated fusion systems
Baoyu Zhang, Shengmin Zhang
math.GR
Nov 1, 2026 · v1
math.AT math.CT math.RT
TL;DR
The main theorem and corollary are formalised unconditionally in Lean (about 62k lines, with Codex assistance) alongside Rocq, and checked with Nanoda and comparator.
Abstract
We prove the Díaz$\unicode[Arial]{x2013}$Park conjecture for sharpness of saturated fusion systems. More generally, for every saturated fusion system $\mathcal F$ over a finite $p$-group and every Mackey functor for $\mathcal F$ over the localisation $\mathbb{Z}_{(p)}$ of the integers at $p$, the higher limits of its contravariant part over the centric orbit category vanish in all positive degrees. In particular, the subgroup and normaliser decompositions of every $p$-local finite group $(S,\mathcal F,\mathcal L)$ over the $\mathcal F$-centric subgroups are sharp. This answers in the affirmative a question in the list of important open problems in [M. Aschbacher, R. Kessar and B. Oliver, Fusion Systems in Algebra and Topology, Cambridge Univ. Press (2011)], and proves the sharpness conjecture stated in [M. Aschbacher and B. Oliver, Fusion systems, Bull. Amer. Math. Soc. (2016)] and Conjecture 1.2 of [E. Yalç$\unicode[Arial]{x131}$n, Higher limits over the fusion orbit category, Adv. Math. (2022)]. The proof is algebraic and does not rely on the classification of finite simple groups.
Problem
The Díaz–Park sharpness conjecture asserts that higher limits of Mackey functors over the centric orbit category of a saturated fusion system vanish in positive degrees. It was listed as an important open problem in the theory of fusion systems.
Approach
The proof is algebraic and avoids the classification of finite simple groups. It works by induction on |S| over all saturated fusion systems, using quotients by central subgroups, centralisers of elementary abelian subgroups and simple Mackey functors over F_p. It then lifts the result to Z_(p) using Nakayama's lemma. The main results were formalised in Lean and Rocq with AI assistance (Codex), and the formal proofs were checked with Nanoda, coqchk and the Lean comparator tool.
Results
Higher limits vanish in all positive degrees for every saturated fusion system and every Mackey functor over Z_(p). As a consequence, the subgroup and normaliser decompositions of p-local finite groups are sharp. The formal development comprises 61,849 lines of Lean in 957 modules and 99,857 lines of Rocq, using only standard axioms.
