Formalizing Pick's Theorem, efficiently

Michael Eisermann

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 sta…