The Harborth constant of Cp ⊕ Cp for every prime p ≥ 11

The Harborth constant $\mathsf g(G)$ of a finite abelian group $G$ is the least $k$ such that every $k$-element subset of $G$ contains $\exp(G)$ distinct elements whose sum is zero; the exponent $\exp(G)$ is the largest order of an element of $G$. Gao and Thangadurai conjectured that $\mathsf g(C_n\oplus C_n)=2n-1$ for odd $n$, and proved it for primes $p\ge 67$; Gao, Geroldinger and Schmid extended this to $p\ge47$, and Kemnitz had settled $p\in\{3,5,7\}$. Bajnok's Menu of research problems asks for the primes $11\le p\le 43$ (Problem F.100). We prove that $\mathsf g(C_p\oplus C_p)=2p-1$ for every prime $p\ge11$, which answers that problem and, with Kemnitz's values, gives the conjecture for every odd prime. As in the work of Gao and Thangadurai and of Gao, Geroldinger and Schmid, we project the set along a line through $0$, which sorts its points into $p$ parallel lines (fibers), choose a projection in which many pairs of points share a fiber, and use the lifting criterion of Gao and Thangadurai. What is new is a sufficient condition, proved with the theorem of Dias da Silva and Hamidoune, that depends only on how many points each fiber holds and not on where the fibers lie. The analysis of fiber sizes is by hand for $p\ge17$ and a finite check for $p=11$ and $13$. The proof for $p\ge11$ and the lower bound for every odd prime are formalized in Lean. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction.

Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.