Formalizing Pick's Theorem in Isabelle/HOL

Sage Binder; Katherine Kosaian

doi:10.48550/arxiv.2405.01793

Back

Formalizing Pick's Theorem in Isabelle/HOL

Preprint

Open access

Formalizing Pick's Theorem in Isabelle/HOL

Sage Binder and Katherine Kosaian

ArXiv.org

Cornell University

05/03/2024

DOI: 10.48550/arxiv.2405.01793

Files and links (1)

url

https://doi.org/10.48550/arxiv.2405.01793View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem in HOL Light, but tailor our proof approach to avoid a primary challenge point in his formalization, which is proving that any polygon with more than three vertices can be split (in its interior) by a line between some two vertices. We detail the approach we use to avoid this step and reflect on the pros and cons of our eventual formalization strategy. We use the theorem prover Isabelle/HOL, and our formalization involves augmenting the existing geometry libraries in various foundational ways (e.g., by adding the definition of a polygon and formalizing some key properties thereof).

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Formalizing Pick's Theorem in Isabelle/HOL
Creators: Sage Binder
Katherine Kosaian
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2405.01793
ISSN: 2331-8422
Publisher: Cornell University; Ithaca, New York
Language: English
Date posted: 05/03/2024
Academic Unit: Computer Science
Record Identifier: 9984696831202771

Metrics

4 Record Views