Формально верифицированное пересечение 3D CSG-сеток: доверяйте 93 строкам спецификации, а не коду ИИ

Новый проект, verified-3d-mesh-intersection, реализует формально верифицированное пересечение 3D-сеток на основе конструктивной сплошной геометрии (CSG) в Lean 4. Ключевая идея: доверять только 93 строкам формальной спецификации, а не 1000+ строкам кода, написанного ИИ. ИИ автоматически написал более 60 000 строк доказательств Lean, которые никогда не требуют проверки человеком — верификатор Lean гарантирует корректность на этапе компиляции.

Как это работает

Спецификация точно определяет поверхность результирующей сетки и гарантирует условия корректности триангуляции. Основное тождество:

solid (meshIntersect M1 M2) = solid M1 ∩ solid M2

где solid представляет бесконечное множество точек внутри сетки. Lean может рассуждать о таких бесконечных множествах и точно доказывать равенство.

Ключевые детали

• Язык: Lean 4, скомпилирован в WebAssembly через emcc-wasm.sh.
• Производительность: 24 секунды на пересечение двух сеток Stanford bunny по 70k треугольников. Медленно, но приоритет — верификация, а не скорость.
• Веб-демо: Запускает верифицированное ядро в браузере по адресу schildep.github.io/verified-3d-mesh-intersection. Поддерживает импорт STL. Данные не отправляются на сервер.
• Проверка человеком: Только 93 строки спецификации требуют чтения. 1000+ строк реализации ИИ и 60k+ строк доказательств ИИ считаются черными ящиками.
• Корректность: Если входные данные некорректны (например, незамкнуты или самопересекаются), алгоритм должен обнаружить это и правильно сообщить — формализовано в спецификации.

Для кого это

Для разработчиков, работающих с 3D-геометрией, CSG-операциями или формальной верификацией, особенно тех, кто скептически относится к доверию коду, сгенерированному ИИ, без гарантий.

Архитектура

Репозиторий содержит ядро Lean (CSG/), обертку на C (wrapper.c) и связующий код для веба (web/). Команды сборки предоставлены через lakefile.lean, emcc-wasm.sh и build_web_demo.sh. UI и связующий код не формально верифицированы.