Formalizing Pick's Theorem in Isabelle/HOL

TL;DR

This work formalizes Pick's theorem in Isabelle/HOL, establishing that the area of a simple polygon with vertices on the integer lattice equals $I + \frac{B}{2} - 1$, where $I$ is the number of interior lattice points and $B$ the boundary lattice points. The authors adopt a strong-induction framework on the number of vertices, base the triangle case on unimodular transformations, and separate the inductive step into convex and non-convex cases; crucially, they avoid Harrison's difficult interior-splitting lemma in the non-convex setting by constructing a pocket outside the polygon via its convex hull and proving the resulting shapes are valid polygons. They contribute substantial formalization work, including a formal definition of polygons, augmentation of geometry libraries, and new lemmas connecting polygonal paths, convex hulls, and interior/exterior notions, ultimately proving the top-level Pick's theorem within the Lebesgue-measurable interior. The work discusses the trade-offs of this approach versus the HOL Light proof, reflects on potential limitations, and outlines future directions such as exploring related geometric results (e.g., the Shoelace formula) and further library enhancements. Overall, this represents a novel, library-expanding formalization of a classic geometric-number-theoretic result in Isabelle/HOL with careful handling of non-convex cases via a pocket construction.

Abstract

We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem in HOL Light, but tailor our proof approach to avoid a primary challenge point in his formalization, which is proving that any polygon with more than three vertices can be split (in its interior) by a line between some two vertices. We detail the approach we use to avoid this step and reflect on the pros and cons of our eventual formalization strategy. We use the theorem prover Isabelle/HOL, and our formalization involves augmenting the existing geometry libraries in various foundational ways (e.g., by adding the definition of a polygon and formalizing some key properties thereof).

Figures (10)

• Figure 1: We visualize the five lattice points inside the polygon in green and the nine points on the boundary in blue, and the area of the polygon is $5 + 9/2 -1 = 8.5$.
• Figure 2: Splitting a polygon with a good linepath and a good polygonal path.
• Figure 3: Applying 1000 1000 1000 1000 1000 1000 pick_union twice.
• Figure 4: Finding a good linepath in a convex polygon with more than three vertices, when the convex hull has three extreme points (left) and more than three extreme points (right). Note that even though the polygon on the left is geometrically a triangle, it is formally a quadrilateral, as it has four vertices ($a$, $b$, $c$, and $d$).
• Figure 5: The blue polygon is $p$, the orange polygon is a pocket, and the orange linepath from $v_1$ to $v_6$ is $\ell$, the "filling linepath". The vertex list $[v_1, v_6, v_7, \dots, v_{13}, v_1]$ generates the filled polygon. Dotted orange lines visualize the other pockets.