A formal proof of Pick's theorem

Mathematical Structures in Computer Science, vol. 21, pp. 715-729, 2011.

Abstract:

Pick's theorem relates the area of a simple polygon with vertices at integer lattice points to the number of lattice points in its inside and boundary. We describe a formal proof of this theorem using the HOL Light theorem prover. As sometimes happens for highly geometrical proofs, the formalization turned out to be more work than initially expected. The difficulties arise mostly from formalizing the triangulation process for an arbitrary polygon.

PDF

Bibtex entry:

@ARTICLE{harrison-pick,
        author          = "John Harrison",
        title           = "A formal proof of Pick's theorem
                           (extended abstract)",
        journal         = "Mathematical Structures in Computer Science",
        volume          = 21,
        year            = 2011,
        pages           = "715-729"}