The maximum area of the convex hull of a polyhex
In the authors' words
A polyhex is an edge-connected set of n cells of the regular hexagonal tiling, where each cell has area one. We prove that the convex hull of a polyhex has area at most (1/6)*ceiling(n^2 + 14n/3), and we show that some polyhex reaches this bound for every n. This proves a conjecture of Kurz from 2008, which asked for the weaker bound (1/6)*floor(n^2 + 14n/3 + 1). The two bounds differ exactly when 3 divides n. We checked the upper bound in the Lean 4 proof assistant with the Mathlib library. We also report a computation over all polyhexes with at most 12 cells, which shows that for these sizes only one shape reaches the maximum, up to rotation and reflection.
Appeared: Monday, September 28. arXiv. Preprint, not yet peer-reviewed.
Authors' comment: 8 pages. Proves Conjecture 2 of Kurz (Beitraege Algebra Geom. 49 (2008)) in a sharpened form. Upper bound formally verified in Lean 4 with Mathlib; code at https://github.com/pragyaangaur/Polyhex-Hull. The maximum areas form OEIS A399934