← All papers
Formalizing Pick's Theorem, efficiently
math.GT
Mar 24, 2026 · v1
TL;DR
Pick's theorem is reformulated as an algebraic identity over an ordered field and the resulting proof is implemented in Lean.
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.
Problem
Pick's theorem (area of an integer polygon by counting lattice points) is notoriously difficult to translate from geometric intuition into a formal rigorous proof.
Approach
The authors transform the geometric reasoning into algebraic form suitable for formalization. They work over an arbitrary ordered field, showing that rational numbers suffice, and implement the algebraic proof in Lean. The approach avoids direct use of Jordan's curve theorem by working with oriented areas and winding-number-like quantities.
Results
Pick's theorem is fully formalized in Lean with an algebraic proof that works over any ordered field, covering both the real and rational cases simultaneously.