Это первая в мире формально верифицированная реализация алгоритма пересечения для многоугольников. Весь код написан на Lean 4, а корректность доказана с помощью Lean checker — никакого классического тестирования, которое не может покрыть все редкие конфигурации.
Мультиполигон задаётся списком внешних контуров и дыр, каждый — набором вершин. Он описывает двумерную область: внутренние точки, формально определённые через чётность пересечений с лучами. Задача — построить новый мультиполигон, внутренность которого равна пересечению внутренностей двух исходных. Поскольку возможных конфигураций бесконечно, только формальная верификация гарантирует равенство для любых входов.
Доверие к корректности строится на двух вещах: Lean checker и ревью человеком трёх коротких файлов — DataStructures.lean, Defs.lean и MultipolygonIntersectionAlgorithmWithPreconditionCheck.lean. Это всего 87 строк простой спецификации. Сам алгоритм (пока неоптимизированный) больше и сложнее, но его читать не нужно — верификация гарантирует, что он выполняет спецификацию. Код будет расти с оптимизациями, а спецификация останется прежней. Все остальные файлы с доказательствами (...Proofs.lean и ...Impl.lean) написаны AI-агентами и никогда не проверялись человеком — в этом нет необходимости благодаря Lean.
Работа с AI-агентами сильно изменилась с выходом новых моделей. Первая попытка в начале года на Claude Opus 4.5 и 4.6: модель могла перевести на Lean только идеально разжёванное доказательство. Например, доказательство независимости определения «внутри» от направления луча пришлось разбить на тысячи строк. Затем вышла Opus 4.7 — она делала более крупные шаги, но всё ещё требовала подсказок (идея с эйлеровыми циклами, обработка особых случаев). А вот Opus 4.8 в ultracode mode справилась сама за несколько часов: параллельно переписала всё доказательство с нуля без единой подсказки и расширила алгоритм для перекрывающихся сегментов, где предыдущая версия застряла. При этом Opus 4.8 лучше оценивала риск: если промежуточная лемма оказывалась неверной, она не висла, а меняла стратегию или запускала параллельных саб-агентов.
Есть и минус: погоня за формальной верификацией часто делает код медленнее и игнорирует практические соображения, не заложенные в спецификацию. Вероятно, из-за нехватки формально верифицированного софта в тренировочных данных.
Попробовать алгоритм можно в веб-демо на основе верифицированного ядра (WebAssembly). Для воспроизведения потребуется elan, а в lean-toolchain зафиксирована leanprover/lean4:v4.15.0. Важно проверять аксиомы, от которых зависят теоремы, — агенты могли случайно протащить лишние. Доверенные аксиомы: [propext, Classical.choice, Quot.sound].
Ранее, в 2021 году, Ди Вито и Хокинг верифицировали в PVS алгоритм слияния простых полигонов, но он работал только с одним внешним контуром и без дыр.