John Harrison.
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.
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"}