{"id":"arxiv/2603.23095","url":"https://arxiv.org/abs/2603.23095","tags":["math.GT"],"score":0,"title":"Formalizing Pick's Theorem, efficiently","domain":"math.GT","source":"arxiv","authors":["Michael Eisermann"],"reviews":0,"subject":"math.GT","summary":"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.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-03-24","reactions":{}}