Formalizing Pick’s Theorem in Isabelle/HOL

Sage Binder

1University of Iowa, Iowa City IA 52242, USA

[email protected] Iowa State University, Ames IA 50011, USA
²²email: [email protected] Katherine Kosaian

Iowa State University, Ames IA 50011, USA
²²email: [email protected]22

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).

Keywords:

Pick’s theorem Isabelle/HOL formalization geometry.

1 Introduction

Pick’s theorem is a gem of late nineteenth-century mathematics, first proved by George Pick in 1899. It concerns simple polygons (i.e., polygons with no self-intersections or holes) whose vertices are integral lattice points and gives a simple-to-state relationship between a polygon’s area and the number of integral lattice points within and on the boundary of the polygon. Pick’s theorem has a number of interesting applications in geometry as well as in number theory [15], but the main reason for its beloved status is arguably the elegant simplicity of the theorem statement. Perhaps for this reason, it was included on the list of “Top 100 Theorems” compiled by Paul and Jack Abad, and is currently tracked in Freek Wiedijk’s corresponding list of “Formalizing 100 Theorems” [27], which tracks which of these theorems have been formalized in (some of the major) theorem provers. In this list, only one theorem—Fermat’s Last Theorem—has not been formalized in any theorem prover, and most have been formalized in multiple provers. Pick’s theorem is one of the few listed theorems which have only been formalized in one prover, namely HOL Light (by John Harrison) [12].

We suspect that the inherent challenge in formalizing geometry has something to do with why Pick’s theorem has only been formalized in one theorem prover. Harrison comments on this challenge in his work [12]. Informal geometric arguments often rely on proof-by-picture intuition, and formalizing these arguments involves working with abstract definitions which are often unwieldy and rather removed from geometric intuition. Consequently, it is not uncommon for the geometry libraries of a theorem prover to be less well-developed than libraries for other areas of mathematics, such as algebra and analysis.

We formalize Pick’s theorem in Isabelle/HOL [19, 18]. Our work is inspired by Harrison’s, but motivated by an interest in avoiding the challenge point of proving that any polygon with more than three vertices can be split into two polygons by a line between two of its vertices. Harrison identifies this step as being particularly arduous, and comments that the proof of Pick’s theorem is significantly simpler for convex polygons [12]. Our approach (discussed in Sect. 3) splits the proof into the convex and non-convex cases; in the non-convex case, we construct a path between two vertices of the polygon that lies fully outside the polygon. In the process, we make various contributions to the Isabelle libraries, such as the formal definition of a polygon and properties of polygons (formalization details are discussed in Sect. 4). Ultimately, we encounter difficulties similar to those discussed by Harrison, and thus do not claim that our approach is simpler than his (we give a retrospective analysis in the conclusion, Sect. 5). Nevertheless, our proof is a novel formalization of Pick’s theorem, and our treatment of the non-convex case involves various creative steps.

Isabelle/HOL, our theorem prover of choice, is well-suited to formalizing mathematics. Our work is facilitated by Isabelle’s automated proof search, particularly Sledgehammer [21], and existing library search tools, particularly SErAPIS [25]. We simultaneously benefit from key results that are already formalized in Isabelle’s libraries and suffer from the library’s foundational gaps. For example, we use the Jordan curve theorem and a variant, called the Jordan triple curve theorem, which are already proved in Isabelle/HOL (and, further, have been specialized to our setting of $\mathbb{R}^{2}$ ). On the other hand, we did not find an existing notion of a polygon in the libraries.

Our formalization is about $14300$ lines of code, and is available on the Archive of Formal Proofs (AFP) [3].

2 Related Work

In Isabelle/HOL’s Archive of Formal Proofs (AFP)¹¹1https://www.isa-afp.org, which is a large centralized repository of proof developments, there are 22 entries categorized under “Mathematical Geometry”²²2https://www.isa-afp.org/topics/mathematics/geometry/ (some entries with a geometric flavor are categorized elsewhere, e.g. a recent formalization [14] of the Poincaré-Bendixson theorem which required formalizing proofs-by-picture is categorized under “Analysis”). Notably, Isabelle’s libraries already contain some results about triangles—in particular, there is a library containing some basic properties of triangles [9], and further results have been proved on top of this, including the intersecting chords theorem [5], Stewart’s theorem [6], and most recently Ceva’s theorem [23]. The underlying triangle library [9] defines a triangle as three points in a real inner product space, but in our setting, it is more natural to define triangles (and general polygons) in terms of their boundary. The formalization of Ceva’s theorem [23] contains a notion of area for triangles, but it is defined in terms of the side lengths of the triangle and the measure of one of the angles. In our formalization, we instead treat area as the Lebesgue measure of the inside of a polygon. Outside of the AFP, implementing (but not verifying) an algorithm to triangulate a polygon was the subject of a recent master’s thesis [24].

Among theorem provers, HOL Light has particularly well-developed geometry libraries [13], and a portion of the geometry results formalized in Isabelle have been ported from HOL Light, including the Jordan curve theorem (formalized by Hales in 2007 [11] and later ported to Isabelle by Paulson), and Euler’s Polyhedron Formula (ported to Isabelle in 2023 by Paulson [20]). Some Euclidean geometry is formalized in Lean’s MathLib, including properties of triangles similar to those in Isabelle [17]; in 2022 Myers formalized the solution to a 2019 geometric IMO problem in Lean [16]. In Coq, some algorithms for triangulating convex hulls have been formalized [2, 8], and many results in Euclidean geometry founded on Tarski’s geometry axioms have been formalized in the GeoCoq library [1] (which has been partially ported to Isabelle/HOL [7]).

3 Our Proof Approach

Pick’s theorem [22] says that the area of a simple polygon whose vertices are integral lattice points is equal to the number of integral lattice points inside the polygon, plus half the number of integral lattice points on the boundary, minus $1$ (see Fig. 1). The standard proof of Pick’s theorem proceeds by (strong) induction on the number of vertices of a polygon, and involves splitting the polygon into two smaller polygons in the inductive step. While we largely follow this standard proof (which is also the approach that Harrison takes), we sidestep the need to prove that any polygon with more than three vertices can be split, so as to avoid a number of painful challenges [12] which Harrison encountered.

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

The high-level structure in our proof is as follows. Let $p$ be a polygon. We proceed by strong induction on the number of vertices defining $p$ . In the base case, we prove Pick’s theorem for triangles (polygons with three vertices). In the inductive case, where the polygon has more than three vertices, we depart from Harrison’s approach by splitting into two subcases: when $p$ is convex, and when $p$ is not convex. We choose to case on convexity since it is mathematically trivial to show that a convex polygon (with more than three vertices) can be split into two smaller polygons on which we can induct. In the non-convex case, we use the convex hull of the polygon to find a linepath lying entirely outside the polygon, which avoids the need to split an arbitrary non-convex polygon. This avoids specific challenges Harrison faced in his formalization, but also presents new challenges of a similar flavor, which we solve with a new approach.

We first discuss some preliminaries (Sect. 3.1) and then further detail our approach (Sect. 3.2—Sect. 3.4), focusing on the novel aspects of our work, particularly the techniques we use in the non-convex case (Sect. 3.4). We present our top-level result in Sect. 3.5.

3.1 Preliminaries

Formally stating Pick’s theorem requires a formal definition of a polygon as well as notions of area, boundary, and inside. Auspiciously, many of the core geometric definitions used in Harrison’s formalization of Pick’s theorem were already present in Isabelle/HOL’s libraries.

Paths and Convex Hulls.

We build on various properties from the libraries about paths. The library definition of a path is a continuous mapping from the interval $[0,1]$ into some topological space; in our setting, we care about paths in $\mathbb{R}^{2}$ . The libraries provide definitions and lemmas for simple paths,³³3A path which does not intersect itself except potentially at its endpoints. linepaths,⁴⁴4A straight line between two points. and joining paths together. In this paper, we frequently refer to the path image of a given path $p$ , which is defined in the libraries as the image of $[0,1]$ under $p$ .

The libraries also provide convex hull results, where the convex hull of a set $S$ is defined as the minimal convex set containing all of $S$ . Additionally, the libraries provide the definition of an extreme point of a set; intuitively, for a convex hull $H$ of a finite set, an extreme point of $H$ is a “corner” of $H$ . One particularly useful result from the libraries is the Krein-Milman-Minkowski theorem, which states that a compact convex set is the convex hull of its extreme points [26].

Polygon Definition.

The existing library did not cover the definition of a polygon, which we develop. Our formal definition of a polygon mirrors Harrison’s [12]. We introduce the make_polygonal_path function to build a polygonal path given a list of vertices. This function takes as input a list of points (type (real^2) list) and returns a function (of type real $\Rightarrow$ real^2) which continuously maps the interval $[0,1]$ to $\mathbb{R}^{2}$ . More precisely, in Isabelle, we write the following:

fun make_polygonal_path :: "(real^2) list $\Rightarrow$ (real $\Rightarrow$ real^2)" where

"make_polygonal_path [] = linepath 0 0"

| "make_polygonal_path [a] = linepath a a"

| "make_polygonal_path [a,b] = linepath a b"

| "make_polygonal_path (a # b # xs) =

(linepath a b) +++ make_polygonal_path (b # xs)"

Here, on an empty list, make_polygonal_path returns a path, linepath 0 0, whose range is the origin (as a default value). On a singleton list [a], it returns a path whose range is the point a. On a list with two points, it returns the line between those two points. On a list with more than two points, it recursively uses the existing library function +++ to join together paths, ultimately returning a path that passes through those points in the order they are input.⁵⁵5Note that the +++ function introduces a particular parameterization of a path; we comment on this parameterization and challenges it introduces in Sect. 4.1.

We then define the predicate polygon on paths, which (intuitively) holds for a path g iff g is a polygon. Our formal definition in Isabelle is as follows, where polygonal_path g holds iff g is in the range of make_polygonal_path, simple_path g holds iff g is a simple path, and closed_path g holds iff g is a closed path (i.e., it starts and ends at the same point).

definition polygon :: "(real $\Rightarrow$ real^2) $\Rightarrow$ bool" where

"polygon g $\longleftrightarrow$ polygonal_path g $\wedge$ simple_path g $\wedge$ closed_path g"

The Frontier, Interior, and Inside.

We make frequent use of the (standard mathematical notions of) interior and frontier (boundary) of a subset $S$ of a topological space (in our setting, $\mathbb{R}^{2}$ ). We also make use of the relative interior; the relative interior of a set $S$ is the set of all $x\in S$ such that there exists an open set $U$ such that $x\in U\cap\text{aff}(S)\subseteq S$ , where aff(S) is the affine hull of $S$ . In our formalization, we mainly care about the relative interior of the image of a linepath, which is simply the image of the linepath minus the endpoints. All of these concepts are already formalized in Isabelle’s standard libraries.

Pick’s theorem is a statement about the area of the “inside” of a polygon. To establish this notion of inside, we use the Jordan curve theorem (and a variant thereof) from the libraries, which proves that every simple closed curve has an inside and an outside that satisfy some intuitively obvious properties: 1) they are disjoint from each other and from the image of the curve, 2) any point in the plane is either inside the curve, outside the curve, or on the curve, and 3) the image of the curve is the frontier of both its inside and its outside.

Splitting a Polygon.

Our proof of Pick’s theorem relies heavily on (strong) induction and involves splitting a polygon into two smaller polygons. We define a good linepath of a polygon $p$ to be a line between two different vertices of $p$ which lies entirely inside $p$ , except for its endpoints (which are on the frontier of $p$ ). We generalize this notion to a good polygonal path of $p$ , where we replace the linepath with a simple polygonal path. In Fig. 2, we illustrate how a good linepath and a good polygonal path split a polygon into two smaller pieces.

Figure 2: Splitting a polygon with a good linepath and a good polygonal path.

Our definitions of good linepath and good polygonal path are designed to satisfy the hypotheses of the Jordan triple curve theorem, a variant of the Jordan curve theorem which has been formalized in the libraries. Intuitively, the Jordan triple curve theorem makes rigorous the notion of splitting a shape into two disjoint shapes whose union is the original shape.

We set up a lemma called pick_union, which states that if a polygon $p$ splits into polygons $q_{1}$ and $q_{2}$ (either by a good linepath or a good polygonal path), and Pick’s theorem holds for any two of $p$ , $q_{1}$ and $q_{2}$ , then Pick’s theorem holds for the remaining polygon. From the Jordan triple curve theorem, we easily have that the areas of the insides of $q_{1}$ and $q_{2}$ sum to the area of $p$ , and we only have to account for the vertices on the splitting path.

3.2 The Triangle Case

To formalize the base case of our induction, which amounts to formalizing Pick’s theorem for triangles, we follow steps similar to Harrison [12] and induct on $I+B$ , where $I$ is the number of integral lattice points inside $p$ , and $B$ is the number of integral lattice points on the boundary of $p$ .

The base case is where $I+B=3$ , which in particular means $I=0$ and $B=3$ . We prove that every such “elementary triangle” has area $1/2$ in a similar fashion to Harrison: we first show that any linear transformation $L\colon\mathbb{R}^{2}\to\mathbb{R}^{2}$ such that $L(\mathbb{Z}^{2})=\mathbb{Z}^{2}$ has determinant $\pm 1$ , then show that every elementary triangle is the image of the unit triangle under one of these linear transformations (modulo translation), where the unit triangle is the convex hull of $\{(0,0),(0,1),(1,0)\}$ . As the unit triangle has area $1/2$ , so does every elementary triangle, since linear transformations with determinant $\pm 1$ preserve area.

In the inductive step, we have $I+B\geq 4$ . Then either $I\geq 1$ or $B\geq 4$ . If $I\geq 1$ , we split the triangle into three smaller triangles; otherwise, if $B\geq 4$ , we split the triangle into two smaller triangles. In the case where we split into two triangles, we show that the splitting linepath is a good linepath and apply pick_union. In the case where we split into three triangles, we apply pick_union twice to reconstruct the inductive result on the three smaller triangles into the result for the bigger triangle. The second application of pick_union requires “adjoining” two polygons whose boundary intersection is not just a linepath, but a polygonal path of two linepaths (Fig. 3). We make use of our generalization of pick_union to polygonal path splits to prove this.

Figure 3: Applying pick_union twice.

3.3 The Convex Case

In the case when $p$ is convex (and not a triangle), we find a good linepath with which we can split $p$ into two smaller polygons to apply our inductive hypothesis. Mathematically, it is obvious that a convex polygon with more than three vertices has a good linepath—the line between any two non-adjacent vertices is a good linepath. Formally, however, this fact is not immediate, and we outline our approach here.

Let $A$ be the convex hull of the path image of $p$ . Since $p$ is a convex polygon, its inside is the interior of $A$ , and its path image is the frontier of $A$ . To find a good linepath, we first apply the fact that if a linepath $\ell$ between two vertices of $p$ has a non-empty intersection with the interior of $A$ , then $\ell$ is in fact a good linepath. This is a consequence of the following general property of subsets of convex sets: if $B$ is convex and $A\subseteq B$ , then the relative interior of $A$ is a subset of the relative interior of $B$ . This reduces the problem to simply finding a linepath which intersects the interior of $A$ . To do this, we case on the number of extreme points $E$ of the convex hull. As $p$ is a polygon, we have $E\geq 3$ .

If $E=3$ , then there is a vertex $d$ of $p$ which is not an extreme point of $A$ (as we are not in the base case, $p$ has at least four vertices). We then identify the extreme point of $A$ which is not on the same linepath as $d$ , and take the linepath between $d$ and this point; this linepath is a good linepath (illustrated in Fig. 4).

If $E>3$ , we take three distinct extreme points of $A$ , call them $a$ , $b$ , $c$ , and show that one of the linepaths of $T=\emph{\small make\_polygonal\_path}\ [a,b,c,a]$ is a good linepath. For this, it is enough to show that $T$ intersects the interior of $A$ . The argument is as follows. Since we are in the $E>3$ case, the inside of $T$ is a strict subset of the interior of $A$ . So, we can obtain points $x$ inside $T$ and $y$ in the interior of $A$ but outside $T$ . As the linepath from $x$ to $y$ intersects both the inside and outside of $T$ , it must intersect $T$ at some point $z$ (see Fig. 4); this is a simple corollary of a lemma from the formalization of the Poincaré-Bendixson theorem [14]. Since both $x$ and $y$ are in the interior of $A$ , and the interior of $A$ is convex, we conclude that $z$ is in the interior of $A$ , as desired.

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

Having shown that $p$ has a good linepath, we use it to split $p$ and apply our inductive hypothesis to the two resulting polygons (this works because each of our smaller polygons has fewer vertices than our original polygon by construction), then apply pick_union. This proves Pick’s theorem for convex polygons.

3.4 The Non-Convex Case

We start our discussion of the non-convex case by giving some high-level geometric intuition, and then discuss the details of formalizing this intuition. When $p$ is not convex, we let $A$ be the convex hull of the path image of $p$ , and use $A$ to find a linepath $\ell$ between two vertices of $p$ that is fully outside $p$ . In particular, we construct a sublist $\emph{\small pocket\_path\_vts}=[a,x_{1},\dots,x_{m},b]$ of the vertices of $p$ , where $a$ and $b$ are on the frontier of $A$ and each $x_{i}$ is in the interior of $A$ . To simplify our construction, we assume WLOG that this sublist begins at the first vertex of $p$ .⁶⁶6Mathematically, this WLOG assumption is immediate; formally, this requires rotating the vertices of a polygon, which changes its parametrization. Showing that the new parametrization is a simple path is involved; we discuss this in Sect. 4.1.2. Then we let $\ell$ be the linepath from $b$ to $a$ .

Drawing $\ell$ creates a “filled” polygon which is the union of our original polygon and a missing piece of the convex hull, which we call a pocket. This pocket is itself a polygon, formed by the vertex list $[a,x_{1},\dots,x_{m},b,a]$ . Ultimately, then, the construction produces two polygons that satisfy our inductive hypothesis: the pocket and the “filled” polygon. Moreover, pocket_path_vts forms a good polygonal path which splits the filled polygon into the pocket and the original polygon, which we use to apply pick_union. Fig. 5 visualizes an example.

Figure 5: The blue polygon is

p

, the orange polygon is a pocket, and the orange linepath from

v_{1}

v_{6}

\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.

To formalize this argument, we first show that the filled shape, which we call filled, is a polygon; as a corollary of this we obtain that the pocket, which we call pocket, is a polygon. Second, we show that pocket_path_vts is a good polygonal path (and that it splits filled into $p$ and pocket).

3.4.1 Showing that filled is a polygon.

When determining how to formalize that $\ell$ intersects $p$ only at $a$ and $b$ (which is sufficient to show that filled is a polygon), we found it useful to draw various examples where this does not hold, to understand how each violates the properties of our construction; Fig. 6 shows some examples. We orient the figures so that the “filling linepath” $\ell$ is horizontal, as our formalization assumes WLOG that $\ell$ lies on the $x$ -axis.

(a) Contradicts that

b

is on the frontier of

A

(b) Contradicts that

x_{1}

and

x_{2}

are in the interior of

A

p

is simple.

(d) Contradicts that

b

is on the frontier of

A

(e) Contradicts that

x_{2}

is in the interior of

A

(f) Contradicts that

p

is simple.

Figure 6: Examples of

\ell

intersecting

p

at a point other than an endpoint of

\ell

Organizing the various possible contradictory situations illustrated in Fig. 6 into a collection of formal lemmas was challenging. We first preclude the Fig. 6(b) and Fig. 6(e) cases by showing that no $x_{i}$ can have the smallest or largest $y$ -coordinate. We then show that no point on $p$ can have negative $y$ -coordinate, which rules out the cases in Fig. 6(a), Fig. 6(d), and Fig. 6(f). Finally, in the Fig. 6(c) case, we show that $p$ is not simple, a contradiction.

To show that no $x_{i}$ can have the smallest or largest $y$ -coordinate, we simply show that any point on $p$ which has smallest or largest $y$ -coordinate is on the frontier of $A$ . This precludes the cases in Fig. 6(b) and Fig. 6(e). Moreover, we obtain some vertex $y_{r}$ which has smaller $y$ -coordinate than every $x_{i}$ , and some vertex $y_{s}$ which has larger $y$ -coordinate than every $x_{i}$ , which we will use to rule out the other cases.

To show that no point on $p$ can have negative $y$ -coordinate, we assume for contradiction that $y_{r}$ has negative $y$ -coordinate. Assuming WLOG that $r<s$ , we consider where the subpath of $p$ from $y_{r}$ to $y_{s}$ intersects the $x$ -axis. We first prove that neither pocket_path nor the subpath can intersect the $x$ -axis at a point not lying on $\ell$ , as such an intersection would put $a$ or $b$ in the interior of $A$ . This precludes the cases Fig. 6(a) and Fig. 6(d), leaving us with the cases in Fig. 6(c) and Fig. 6(f).

In the Fig. 6(f) case, the subpath and pocket_path intersect the $x$ -axis only on $\ell$ , and here we show that the subpath must intersect pocket_path (which contradicts that $p$ is simple). For this, we construct an axis-parallel rectangle whose lower edge lies on the $x$ -axis, and whose width and height are large enough so that the entire pocket path and subpath are inside the rectangle. Then, we delete the points lying between $a$ and $b$ on the bottom edge of the rectangle and replace the resulting gap by pocket_path (illustrated in Fig. 7); we let $R$ be the resulting closed, simple path. We show that $y_{r}$ is outside $R$ , and that $y_{s}$ is inside $R$ , and this yields (via a lemma from the Poincaré-Bendixson formalization [14]) that the subpath intersects $R$ . However, by the construction of $R$ , the subpath can neither intersect the side edges nor the top edge of $R$ , nor can it intersect the two axis-parallel bottom edges of $R$ . Thus, the only remaining part of $R$ which it can intersect is pocket_path, as desired.

Figure 7: If the subpath and pocket_path intersect the

x

-axis only on

\ell

, then the subpath intersects pocket_path.

Formalizing that $y_{r}$ is outside $R$ and $y_{s}$ is inside $R$ in the above argument is itself a challenge. The construction of $R$ makes this pictorially obvious, but formally, we only know the abstract facts about the inside and outside of $R$ given by the Jordan curve theorem (see Sect. 3.1). Working with the abstract definitions, we show that $y_{r}$ is in the unbounded component of $\mathbb{R}^{2}\setminus R$ (i.e., $y_{r}$ is outside $R$ ) by constructing an infinite ray beginning at $y_{r}$ which never intersects $R$ (a downward vertical ray suffices). To obtain that $y_{s}$ is inside $R$ , we take a sufficiently small $\epsilon$ -ball around the point on $R$ directly above $y_{s}$ , and (using a library result) obtain a point $z$ which is both in this $\epsilon$ -ball and inside $R$ . We then show that $z$ cannot be above the upper edge of $R$ (if it were, it would be outside $R$ , which we show by taking an upward vertical ray). Finally, we take the linepath from $z$ to $y_{s}$ and show that this linepath cannot intersect $R$ ; then, as $z$ is inside $R$ , so is $y_{s}$ . These proof techniques are illustrated in Fig. 7.

So, $y_{r}$ cannot have negative $y$ -coordinate, which establishes that every point on $p$ has non-negative $y$ -coordinate. Then, since $\ell$ lies on the $x$ -axis, $\ell$ lies on the frontier of $A$ . Thus, pocket_path does not intersect $\ell$ at a point other than its endpoints, precluding the Fig. 6(f) case.⁷⁷7This implies that pocket is a polygon, which is used later in the proof that pocket_path is a good polygonal path.

The case in Fig. 6(c) is the only remaining case. We assume for contradiction that $\ell$ minus its endpoints intersects $p$ , and with a bit of work, we can assume in particular that $y_{r}$ lies on $\ell$ . So, we have a subpath (from $y_{r}$ to $y_{s}$ ) of $p$ which starts at a point on $\ell$ and ends at a point above all points on pocket_path, illustrated in Fig. 8. We can then show that this subpath necessarily crosses pocket_path using some of our prior proof techniques (compare Fig. 7).

Figure 8: If all points on

p

are non-negative, we have a subpath of

p

which starts on

\ell

and ends at a point above all points of

p

, and thus

p

intersects itself.

3.4.2 Showing that pocket_path is a good polygonal path of filled.

From the previous result, we have that pocket_path intersects filled only at $a$ and $b$ , and so pocket_path (minus $a$ and $b$ ) is either entirely inside or entirely outside filled.⁸⁸8As we now have that filled is a polygon, we can refer to its inside and outside. Thus, to show that pocket_path is inside filled, it suffices to find only a single point on pocket_path which is inside filled.

We first obtain a point $z$ which is inside both pocket and filled. While it is intuitively clear that the inside of pocket is a subset of the inside of filled, showing this formally requires some machinery. We take an $\epsilon$ -ball around a point on $\ell$ , and obtain points $z$ and $z^{\prime}$ in the $\epsilon$ -ball where $z$ is inside pocket and $z^{\prime}$ is inside filled; this is illustrated in Fig. 9. We ensure that $\epsilon$ is small enough so that the linepath from $z$ to $z^{\prime}$ does not intersect filled, and this shows that $z$ is inside filled.

So, we have that $z$ is inside both pocket and filled, and we take a ray $r$ starting at $z$ , constructed so that $r$ intersects pocket_path at a point $y$ before its first intersection with filled at a point $x$ . As $r$ starts inside filled, all points on $r$ prior to $x$ are inside filled, and thus $y$ is inside filled and on pocket_path. As we know that pocket_path is simple and intersects filled only at $a$ and $b$ , the existence of $y$ suffices to show that pocket_path is a good polygonal path of filled.

Figure 9: The ray

r

, shown in orange, intersects pocket_path at

y

before its first intersection with filled at

x

3.5 Top-Level Result

Putting all the pieces together yields the following top-level result.

theorem pick:

assumes "polygon p" "p = make_polygonal_path vts" "all_integral vts"

assumes "I = card {x. integral_vec x $\wedge$ x $\in$ path_inside p}"

assumes "B = card {x. integral_vec x $\wedge$ x $\in$ path_image p}"

shows "measure lebesgue (path_inside p) = I + B/2 - 1"

This theorem states that if p is a polygon with vertex list vts where all of the vertices in vts are integral lattice points (assumption all_integral vts), and if I is the cardinality of the set of integral points inside p and B is the cardinality of the set of integral lattice points on the boundary of p, then the area of p (given by the Lebesgue measure of its path inside, using Isabelle/HOL’s standard library definitions measure and lebesgue) is I + B/2 - 1, as claimed by Pick’s theorem.

4 Formalization Details

Having outlined our proof approach, we turn to some further details of our formalization, including challenges we faced and library extensions we contribute.

4.1 Polygon Properties

4.1.1 Linepath Characterization of Polygonal Paths.

In the Isabelle libraries, a path is a map from the unit interval $[0,1]$ into some topological space. The library definition of joining two paths $p_{1}$ and $p_{2}$ together, +++, assigns the first half of the unit interval to $p_{1}$ , and the second half to $p_{2}$ . We construct polygons by repeated application of this +++ operation (see Sect. 3.1). This has the effect that the first linepath in a polygonal path corresponds to the interval $[0,\frac{1}{2}]$ , the second linepath to $[\frac{1}{2},\frac{3}{4}]$ , the third linepath to $[\frac{3}{4},\frac{7}{8}]$ , and so forth; the last linepath corresponds to $[\frac{2^{n-1}-1}{2^{n-1}},1]$ , where $n$ is the number of vertices in the polygonal path (see Fig. 10). Harrison also used this parametrization in his work [12]. Using +++ in this way allows us to directly apply library lemmas about joining paths, but we found this parametrization unwieldy to work with in practice.

Figure 10: Paramaterization of a polygonal path with six vertices.

For example, suppose $p=\emph{\small make\_polygonal\_path}\ \emph{\small[a, b, c, d, a]}$ is a polygon. Then we might expect

p^{\prime}=\emph{\small(make\_polygonal\_path [a, b, c]) +++ (make\_polygonal\_path [c, d, a])}

to also form a polygon. While we can show that $p^{\prime}$ is simple and has the same path image as $p$ , $p^{\prime}$ is (unintuitively) not a polygon because of its parametrization. We also encounter challenges when proving that if vts generates a simple polygonal path $p$ , then so does any sublist of length at least two of vts. While library lemmas establish that a subpath of a simple path is simple, our polygon parametrization means that a sublist does not necessarily generate a subpath.

To mitigate such challenges, we ultimately formalized a collection of lemmas that translate between the parametrization of a polygonal path $p$ and the parametrization of its constituent linepaths: given $t\in[0,1]$ , we obtain $t^{\prime}\in[0,1]$ where $p(t)=\ell(t^{\prime})$ and $\ell$ is a linepath of $p$ . Though not overly mathematically complex, this translation was somewhat tedious to formalize and apply.

4.1.2 Polygon Vertex Rotation.

We often found it convenient to assume WLOG that a property which holds for some vertex in a polygon holds for the first vertex. Intuitively, if $p=\emph{\small make\_polygonal\_path}\ \emph{\small[a, b, c, d, a]}$ is a polygon, then it is “essentially” the same polygon as $p^{\prime}=\emph{\small make\_polygonal\_path}\ \emph{\small[b, c, d, a, b]}$ . Though $p$ and $p^{\prime}$ are different curves, they have the same path image and are geometrically the same. However, it was non-trivial to formalize that $p$ is a polygon iff $p^{\prime}$ is a polygon because they are parametrized differently (this was our original impetus to formalize the aforementioned parametrization translation between a polygonal path and its linepaths).

In Isabelle, we formalize rotation on the vertex list of a polygon in the function rotate_polygon_vertices and prove the following crucial properties to establish that rotating a polygon yields a polygon with the same path image.

lemma rotation_is_polygon:

assumes "polygon p" "p = make_polygonal_path vts"

assumes "vts’ = rotate_polygon_vertices vts i"

shows "polygon (make_polygonal_path vts’)" and

"path_image (make_polygonal_path vts’) = path_image p"

4.2 Unit Geometry

In the base case of our induction to prove Pick’s theorem for triangles, we must show that the area of the unit triangle is $1/2$ (see Sect. 3.2). While the formula for the area of a triangle is a grade-school fact, we formally treat the area of a polygon as the Lebesgue measure of its inside, which is not entirely straightforward to work with (given the abstractness of the Lebesgue measure and ‘inside’ definitions). We use existing library results to show that the area of a unit square is $1$ ,⁹⁹9Intuitively, the Lebesgue measure of open rectangles is “hard-coded” in the definition; showing that the area of the unit square is $1$ essentially amounts to showing that the unit square (defined as a convex hull of its four corners) is $[0,1]\times[0,1]$ . and then show that the unit square can be split into the unit triangle and its diagonal mirror. As the unit triangle and its mirror have the same area, and their areas sum to $1$ , they each must have area $1/2$ . Formalizing this involved concretely characterizing the abstract ‘inside’ of the unit triangle and unit square (for example, we prove that the unit triangle is the set of points $(x,y)$ where $0\leq x$ , $0\leq y$ , and $x+y\leq 1$ ) and matching between the various definitions (e.g., the interior of the convex hull of three points is the same as the path inside of the polygon formed by the three points), a task which overall proves more intricate and finicky than grade-school intuition would suggest.

4.3 Convex Hull Properties

In the course of our formalization, we need to prove a variety of general results relating convex hulls to polygons. This can be tricky, since a polygon is a mapping with specific properties, whereas a convex hull is simply a set of points. For example, if we take the convex hull of a polygon (which is the same as taking the convex hull of the vertices of the polygon), then geometrically the result can clearly be characterized as a polygon. In generality, the missing result is that the convex hull of any finite set of points can be alternatively characterized by the path inside of some polygon. Formally establishing this connection is nontrivial; in our proof approach, we formalize a significant step towards this by showing that filling in a pocket of the convex hull yields a polygon.

We additionally contribute other results that augment the existing library support for convex hulls. For example, we prove that if all of the vertices of a polygon are on the frontier of its convex hull, then the polygon itself is convex. In contrapositive, this yields that for a non-convex polygon, some vertex is in the interior of its convex hull, which we use to show that a non-convex polygon has a pocket. While geometrically obvious in a proof-by-picture fashion, the formal proof was more detailed and involved relating the notions of convex hulls, affine hulls, and half planes; in particular, we show that if a linepath is not on the frontier of the convex hull, it “cuts” the convex hull, which then forces a self-intersection in the polygonal path. This notion of “cutting” is different than that afforded by the Jordan triple curve theorem, and its formalization involved characterizing certain intersections of a convex hull with an affine hull of two points, as well as classifying the frontier of half plane as an affine hull.

5 Conclusion and Future Work

Our formalization of Pick’s theorem, the second in any theorem prover, involves both creative strategies to formalize pictorial arguments and considerable fundamental library extensions. The other existing formalization of Pick’s theorem, by John Harrison in HOL Light [12], emphasizes the surprisingly involved nature of formalizing geometry. While we succeeded in avoiding a particularly thorny part of Harrison’s proof by formalizing a less common approach to proving Pick’s theorem, we do not claim that our formalization is overall simpler. Ultimately, we resonate with many of the difficulties Harrison describes. Describing the step to verify the existence of a good linepath in a polygon, Harrison writes “. . . we found it quite hard work reasoning about obvious facts like ‘this point and that point are on opposite sides of the line’.” [12, p. 12]. We encountered a similar difficulty in our formalization, particularly in the piece of our proof that avoided this very step (the non-convex case, Sect. 3.4).

While we believe there are inherent challenges in formalizing geometry, a retrospective analysis also reveals portions of our formalization that were potentially unnecessarily painful. In particular, the difficulties we faced with the parametrization induced by our polygon construction could have potentially (retrospectively) been avoided by using a polygon definition along the following lines: $P\subseteq\mathbb{R}^{2}$ is a polygon iff (1) $P$ is the path image of some (potentially non-simple) polygonal path, and (2) $P$ is the path image of some simple path. Note that this definition treats a polygon as a subset of $\mathbb{R}^{2}$ , not a mapping from $[0,1]$ into $\mathbb{R}^{2}$ . This definition lets us find separate witnesses of the “polygonal-ness” and “simple-ness” of a polygon, which may avoid the problems we encountered in showing that certain vertex transformations of polygons, such as polygon vertex rotation or taking sublists, yield simple polygonal paths.

In addition to exploring potential simplifications of our formalization, there are some interesting possible extensions of our work. Our formalization takes the first step towards showing that any polygon can be made convex by removing some of its vertices (i.e., by filling in its pockets). Further, our formal treatment of pockets opens up the possibility of verifying other theorems about pockets, such as the Erdös-Nagy theorem, which states that any polygon can be made convex by successively picking a pocket and flipping it across the face it shares with the convex hull [10]. We are also interested in other theorems related to area and geometry, e.g. the Shoelace theorem (alternately called the Surveyor’s Formula) [4], and in connecting our work to some of the pre-existing Isabelle results like Ceva’s theorem (which used a different definition of area) [23].

{credits}

5.0.1 Acknowledgements

This material is based upon work supported by the National Science Foundation under Grant No. 1552934. Thank you to Lawrence and Susan Sheets for generously supporting S.B. with a graduate fellowship. Thank you to Aaron Stump and Yong Kiam Tan for useful comments on the paper.

5.0.2 \discintname

The authors have no competing interests to declare that are relevant to the content of this article.

References

[1] Beeson, M., Boutry, P., Braun, G., Gries, C., Narboux, J.: GeoCoq (Jun 2018), https://inria.hal.science/hal-01912024
[2] Bertot, Y.: Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs. In: Fischer, B., Uustalu, T. (eds.) ICTAC. LNCS, vol. 11187, pp. 3–10. Springer (2018). https://doi.org/10.1007/978-3-030-02508-3_1, https://doi.org/10.1007/978-3-030-02508-3_1
[3] Binder, S., Kosaian, K.: Pick’s theorem. Archive of Formal Proofs (April 2024), https://isa-afp.org/entries/Picks_Theorem.html, Formal proof development
[4] Braden, B.: The surveyor’s area formula. The College Mathematics Journal 17(4), 326–337 (1986)
[5] Bulwahn, L.: Intersecting chords theorem. Archive of Formal Proofs (October 2016), https://isa-afp.org/entries/Chord_Segments.html, Formal proof development
[6] Bulwahn, L.: Stewart’s theorem and Apollonius’ theorem. Archive of Formal Proofs (July 2017), https://isa-afp.org/entries/Stewart_Apollonius.html, Formal proof development
[7] Coghetto, R.: Tarski’s parallel postulate implies the 5th postulate of Euclid, the postulate of Playfair and the original parallel postulate of Euclid. Archive of Formal Proofs (January 2021), https://isa-afp.org/entries/IsaGeoCoq.html, Formal proof development
[8] Dufourd, J., Bertot, Y.: Formal study of plane delaunay triangulation. In: Kaufmann, M., Paulson, L.C. (eds.) ITP. LNCS, vol. 6172, pp. 211–226. Springer (2010). https://doi.org/10.1007/978-3-642-14052-5_16, https://doi.org/10.1007/978-3-642-14052-5_16
[9] Eberl, M.: Basic geometric properties of triangles. Archive of Formal Proofs (December 2015), https://isa-afp.org/entries/Triangle.html, Formal proof development
[10] Grünbaum, B.: How to convexify a polygon. Geombinatorics 5(1), 24–30 (1995)
[11] Hales, T.C.: The Jordan curve theorem, formally and informally. Am. Math. Mon. 114(10), 882–894 (2007), http://www.jstor.org/stable/27642361
[12] Harrison, J.: A formal proof of Pick’s theorem. Math. Struct. Comput. Sci. 21(4), 715–729 (2011). https://doi.org/10.1017/S0960129511000089
[13] Harrison, J.: The HOL Light theory of Euclidean space. J. Autom. Reason. 50(2), 173–190 (2013). https://doi.org/10.1007/S10817-012-9250-9, https://doi.org/10.1007/s10817-012-9250-9
[14] Immler, F., Tan, Y.K.: The Poincaré-Bendixson theorem in Isabelle/HOL. In: Blanchette, J., Hritcu, C. (eds.) CPP. pp. 338–352. ACM (2020). https://doi.org/10.1145/3372885.3373833
[15] Kiradjiev, K.: Connecting the dots with Pick’s theorem. Mathematics Today (2018), https://ima.org.uk/10981/connecting-the-dots-with-picks-theorem/, instutite of Mathematics and its Applications
[16] Myers, J.: IMO 2019 Q2. Lean MathLib (2022), https://github.com/leanprover-community/mathlib4/blob/master/Archive/Imo/Imo2019Q2.lean
[17] Myers, J., Candales, M.: Triangles. Lean MathLib (2020), https://github.com/leanprover-community/mathlib4/blob/1c0ac885c9b8aa4daa1830acb56b755140a8059f/Mathlib/Geometry/Euclidean/Triangle.lean
[18] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002). https://doi.org/10.1007/3-540-45949-9
[19] Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363–397 (1989). https://doi.org/10.1007/BF00248324
[20] Paulson, L.C.: Euler’s polyhedron formula. Archive of Formal Proofs (September 2023), https://isa-afp.org/entries/Euler_Polyhedron_Formula.html, Formal proof development
[21] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL. EPiC Series in Computing, vol. 2, pp. 1–11. EasyChair (2010). https://doi.org/10.29007/36DT
[22] Pick, G.: Geometrisches zur zahlenlehre. Sitzenber. Lotos (Prague) 19, 311–319 (1899)
[23] Rabing, M.S.: Ceva’s theorem. Archive of Formal Proofs (August 2023), https://isa-afp.org/entries/Ceva.html, Formal proof development
[24] Skjelnes, M.: Implementation and specification of a simple polygon triangulation algorithm in Isabelle/HOL (2020), https://uu.diva-portal.org/smash/get/diva2:1578586/FULLTEXT01.pdf, Master’s Thesis, Uppsala Universitat
[25] Stathopoulos, Y., Koutsoukou-Argyraki, A., Paulson, L.C.: SErAPIS: A concept-oriented search engine for the Isabelle libraries based on natural language. In: Online proceedings of the Isabelle Workshop affiliated to IJCAR 2020 (virtual) (2020)
[26] Voigt, J.: The Krein–Milman Theorem, pp. 131–138. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-32945-7_17
[27] Wiedijk, F.: Formalizing 100 theorems, https://www.cs.ru.nl/~freek/100/