Formalizing Pick's Theorem, efficiently
Geometric Topology
2026-03-25 v1
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.
Keywords
Cite
@article{arxiv.2603.23095,
title = {Formalizing Pick's Theorem, efficiently},
author = {Michael Eisermann},
journal= {arXiv preprint arXiv:2603.23095},
year = {2026}
}
Comments
9 pages, 9 figures