Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing Pick's Theorem, efficiently

Michael Eisermann

Abstract

Pick's astonishing theorem explains how to obtain the area of any integer polygon by counting lattice points. It is a notoriously difficult challenge to translate the geometric statement and intuitive reasoning into a formal statement and rigorous proof. We transform the beautiful geometry into equally elegant algebra, and then implement the algebraic proof in Lean.

Formalizing Pick's Theorem, efficiently

Abstract

Pick's astonishing theorem explains how to obtain the area of any integer polygon by counting lattice points. It is a notoriously difficult challenge to translate the geometric statement and intuitive reasoning into a formal statement and rigorous proof. We transform the beautiful geometry into equally elegant algebra, and then implement the algebraic proof in Lean.
Paper Structure (11 sections, 5 theorems, 22 equations, 8 figures)

This paper contains 11 sections, 5 theorems, 22 equations, 8 figures.

Table of Contents

  1. Introduction: Pick's wonderful theorem
  2. How to formalize Pick's theorem?
  3. The euclidean angle measure
  4. The discrete angle measure
  5. Proof of Pick's lemma
  6. Axiomatic angle measure
  7. Jordan's decomposition for polygons
  8. Hopf's umlaufsatz for polygons
  9. Formalizing Hopf's umlaufsatz
  10. A “water proof” plausibility argument
  11. Quotes

Key Result

Theorem 1.1

Let $P = (p_0,p_1,\ldots,p_n=p_0)$ be a simply closed polygon with integer vertices $p_i \in \mathbb{Z}^2$. Then $\mathop{\mathrm{vol}}\nolimits_2(B) = I + J/2 - 1$.

Figures (8)

  • Figure 1: (a) rectangle, (b) oblique square, (c) Farey sunburst $F_6$
  • Figure 2: Oriented area of a trapezoid and of a polygon
  • Figure 3: The discrete angle measure
  • Figure 4: Proving $\mathrm{welp}(u,v) = \mathrm{area}(u,v)$ by inspecting $q \mapsto \mathrm{dang}(u-q,v-q)$
  • Figure 5: We transform Pick's Theorem to Pick's lemma
  • ...and 3 more figures

Theorems & Definitions (25)

  • Theorem 1.1: Georg Pick 1899 Pick:1899
  • Example 1.2
  • Remark 1.3
  • Remark 1.4
  • Remark 1.5
  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Remark 2.4
  • Lemma 2.5: Pick's lemma, using the euclidean angle measure
  • ...and 15 more