Formalizing Pick's Theorem in Isabelle/HOL

TL;DR

This paper formalizes Pick's theorem within Isabelle/HOL, providing a rigorous proof for calculating polygon areas on integer lattices while addressing challenges in polygon splitting proofs.

Contribution

It introduces a novel formalization approach in Isabelle/HOL that avoids complex splitting proofs present in prior work, enhancing the robustness of formal geometric reasoning.

Findings

Successful formalization of Pick's theorem in Isabelle/HOL

Development of augmented geometry libraries for polygon properties

Insights into proof strategies avoiding complex splitting steps

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