Formalizing Pick's Theorem, efficiently

TL;DR

This paper formalizes Pick's Theorem, transforming its geometric intuition into algebra and implementing a rigorous proof in Lean to enhance mathematical rigor and computational verification.

Contribution

It provides a formal algebraic proof of Pick's Theorem in Lean, bridging geometric intuition and formal verification.

Findings

Successful algebraic formalization of Pick's Theorem

Implementation of the proof in Lean proof assistant

Enhanced rigor and reproducibility in geometric proofs

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.