Формальное доказательство теоремы Пика

Теорема Пика связывает площадь простого многоугольника с вершинами в узлах целочисленной решётки с количеством узлов решётки, расположенных внутри многоугольника и на его границе. Мы описываем формальное доказательство этой теоремы с использованием системы доказательства теорем HOL Light. Как это иногда бывает с геометрическими доказательствами, формализация потребовала больше усилий, чем предполагалось первоначально. Основные трудности возникли при формализации процесса триангуляции произвольного многоугольника.