多六边形凸包的最大面积
The maximum area of the convex hull of a polyhex
浏览论文内容
中文总结 AI 辅助
本文证明多六边形凸包面积上界为 (1/6)*ceiling(n^2+14n/3)，并验证达到该界的形状存在，解决了 Kurz 2008 年的猜想，同时用 Lean 4 验证并计算了小尺寸下的唯一极值形状。
中文摘要 AI 辅助
多六边形是正六边形平铺中 n 个边连通单元组成的集合，其中每个单元面积为 1。我们证明多六边形的凸包面积至多为 (1/6)*ceiling(n^2 + 14n/3)，并表明对每个 n 都存在某个多六边形达到此上界。这证明了 Kurz 在 2008 年提出的猜想，该猜想要求更弱的界 (1/6)*floor(n^2 + 14n/3 + 1)。这两个界恰好当 3 整除 n 时不同。我们在 Lean 4 证明助手和 Mathlib 库中检查了上界。我们还报告了对至多 12 个单元的所有多六边形的计算，结果表明对于这些尺寸，仅有一个形状（在旋转和反射意义下）达到最大值。
英文摘要
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.
