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

### License

### Topics

### Related publications

- Grunbaum, B., & Shephard, G. C. (1993). Pick’s Theorem. The American Mathematical Monthly, 100(2), 150. https://doi.org/10.2307/2323771
- HARRISON, J. (2011). A formal proof of Pick’s Theorem. Mathematical Structures in Computer Science, 21(4), 715–729. https://doi.org/10.1017/s0960129511000089

### Session Picks_Theorem

- Integral_Matrix
- Polygon_Jordan_Curve
- Polygon_Lemmas
- Linepath_Collinearity
- Polygon_Convex_Lemmas
- Polygon_Splitting
- Triangle_Lemmas
- Unit_Geometry
- Elementary_Triangle_Area
- Pick