Article contents
A formal proof of Pick's Theorem
Published online by Cambridge University Press: 01 July 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 formalisation turned out to be more work than initially expected. The difficulties arose mostly from formalising the triangulation process for an arbitrary polygon.
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 21 , Special Issue 4: Interactive Theorem Proving and the Formalisation of Mathematics , August 2011 , pp. 715 - 729
- Copyright
- Copyright © Cambridge University Press 2011
References
![](https://static.cambridge.org/binary/version/id/urn:cambridge.org:id:binary:20151022124959644-0233:S0960129511000089_char1.gif?pub-status=live)
- 2
- Cited by