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

John Harrison.

In Fukuda et al. (eds) "Proceedings of ICMS 2010", Springer LNCS vol. 6327, 2010.
This is superseded by the corresponding full paper

Abstract:

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 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.

PDF

Bibtex entry:

@INPROCEEDINGS{harrison-picka,
        author          = "John Harrison",
        title           = "A formal proof of Pick's theorem
                           (extended abstract)",
        editor          = "Komei Fukuda and Joris van der Hoeven and
                           Michael Joswig and Nobuki Takayama",
        booktitle       = "Proceedings of ICMS 2010, the Third International
                           Congress on Mathematical Software",
        address         = "Kobe, Japan",
        date            = "September 2010",
        publisher       = "Springer-Verlag",
        series          = "Lecture Notes in Computer Science",
        volume          = 6327,
        year            = 2010,
        pages           = "152--154"}