Formalizing Pick's Theorem, efficiently
arXiv:2603.23095
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.
9 pages, 9 figures