The Díaz-Park sharpness conjecture asserts that certain higher inverse limits of Mackey functors for saturated fusion
systems vanish (Díaz and Park 2015). A fusion system 
on a finite p-group 
is a category whose objects are the subgroups
of 
and whose morphisms are specified injective group
homomorphisms. Saturation imposes extension and Sylow
p-subgroup conditions on automorphism
groups. The centric orbit category 
restricts the fusion orbit category 
to subgroups whose 
-conjugates have centralizer
in 
equal to their group center.
For a Mackey functor 
on the full fusion orbit category 
with values in finite-dimensional vector
spaces over the finite field 
, the conjectured vanishing is
 |
for every 
, where 
is the contravariant
functor part restricted to the centric orbit
category.
Zhang and Zhang (2026) report the vanishing for all Mackey functors valued in modules over 
, the localization
of the integers at 
. This includes the original finite-dimensional case.
Shengmin Zhang reports using ChatGPT to find an initial candidate proof,
and Baoyu Zhang reports using Codex for the Lean and Rocq formalizations. The project
reports checks of the formal proofs using Nanoda and coqchk (Zhang 2026).
