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

BSD License

### Topics

- Mathematics/Geometry

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

### Depends on

- The Poincaré-Bendixson Theorem

### Auto-related entries

- Bertrand’s postulate
- Basic Geometric Properties of Triangles
- Fourier Series
- Ptolemy’s Theorem
- The Cartan Fixed Point Theorems

## Cite

×

Picks_Theorem-AFP

    @article{Picks_Theorem-AFP,
      author  = {Sage Binder and Katherine Kosaian},
      title   = {Pick's Theorem},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2024},
      note    = {\url{https://isa-afp.org/entries/Picks_Theorem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest