Pick's Theorem

Sage Binder 🌐 and Katherine Kosaian 🌐

April 26, 2024


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


BSD License


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