A formal proof of Pick's theorem
Mathematical Structures in Computer Science, vol. 21, pp. 715-729, 2011.
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
author = "John Harrison",
title = "A formal proof of Pick's theorem
journal = "Mathematical Structures in Computer Science",
volume = 21,
year = 2011,
pages = "715-729"}