The paper solves a specific problem in combinatorial group theory about the Heisenberg group of order 343. The Heisenberg group here refers to a group of 3x3 upper triangular matrices with entries from a finite field with 7 elements. The central question is: what is the longest sequence of elements from this group such that no subset of them, in any order, multiplies together to give the identity element? This quantity is called the small Davenport constant. Researchers had conjectured that for these Heisenberg groups the answer follows a simple formula, and the paper confirms this for the 343 case, showing the answer is exactly 18.
The proof has two parts. Showing the constant is at least 18 is done by explicitly constructing a sequence of 18 elements with the required property. The harder part is showing no sequence of length 19 can work. To do this, the authors organize all hypothetical length-19 sequences into categories based on structural features, specifically how many elements fall in the center of the group and how the remaining elements spread across geometric directions in a related simpler object. Some categories are ruled out by theoretical reasoning, while others require exhaustive computer search.
Because the computer search is central to the proof, the authors put significant effort into making it trustworthy. They used a SAT solver, a tool that decides whether logical constraints can be satisfied, to check the remaining cases, and they generated formal certificates that an independent program verified step by step. They also built a separate audit system to double-check the problem encoding, the stored proofs, and the explicit construction. The result fits neatly into a broader pattern: the conjecture that the small Davenport constant equals 3p minus 3 for these groups now holds for the primes 3, 5, and 7.