Lean 4 proof of Kurz's conjecture on the maximum convex hull area of polyhexes. The result is now OEIS A399934.
computational-geometry lean combinatorics oeis polyhexes mathematical-proof oeis-a399934 principia-math
-
Updated
Oct 6, 2026 - Lean