← All papers

The maximum area of the convex hull of a polyhex

Pragyaan Gaur

math.CO Sep 23, 2026 · v1 math.MG

formalization combinatorics geometry

Read PDF arXiv abstract Code

TL;DR

The upper bound on the convex-hull area of polyhexes was formalized in Lean 4 with Mathlib, using Lebesgue measure.

Abstract

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.

Problem

Determine the maximum area of the convex hull of a polyhex (an edge-connected set of n regular unit hexagons), proving a 2008 conjecture of Kurz.

Approach

The hull is written as a Minkowski sum P+H in axial coordinates on the triangular lattice, reducing area to widths of the cell-centre hull. Spanning-tree estimates bound P's area via edge counts, giving the tight upper bound M(n)=(1/6)ceil(n^2+14n/3). The upper bound was formalized in Lean 4 with Mathlib, defining cells as integer points, area as Lebesgue measure, and proving the hexagon has area one and the coordinate map has determinant one.

Results

The maximum area equals (1/6)ceil(n^2+14n/3), confirming (and slightly sharpening) Kurz's conjecture, with a Lean development containing no unproved steps using only the three standard axioms. A brute-force enumeration over all polyhexes with at most 12 cells confirms the bound and shows a unique maximizing shape up to symmetry.

n	fixed polyhexes	6M(n)	maximisers (free)
1	1	6	1
2	3	14	1
3	11	23	1
6	814	64	1
12	8182213	200	1

Search results over polyhexes with at most n cells: maximum hull area 6M(n) and number of free maximisers.

Papers With

The maximum area of the convex hull of a polyhex