A formal proof of Pick's theorem (extended abstract)

Abstract

Given a polygon with vertices at integer lattice points (i.e. where both x and y coordinates are integers), Pick's theorem [4] relates its area A to the number of integer lattice points I in its interior and the number B on its boundary: A=I+B/2-1 We describe a formal proof of this theorem using the HOL Light theorem prover [2]. As sometimes happens for highly geometrical proofs, the formalization turned out to be quite challenging. In this case, the principal difficulties were connected with the triangulation of an arbitrary polygon, where a simple informal proof took a great deal of work to formalize. © 2010 Springer-Verlag.