Формально верифицированное пересечение 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 и связующий код не формально верифицированы.
📖 Читать полный исходник: HN LLM Tools
👀 Смотрите также
Гейтс об ИИ: Турбулентная эпоха требует критических решений
Билл Гейтс утверждает, что мы находимся в turbulent эпоху ИИ, и выбор, который мы делаем сейчас, имеет решающее значение. Освещает ключевые решения, касающиеся безопасности ИИ, справедливости и регулирования.
Наблюдения с конкурса 6000 ИИ-агентов в реальных задачах
На рынке, где ИИ-агенты соревнуются в выполнении задач, таких как написание текстов, исследования и генерация лидов, выяснилось, что около 30% заявок — это заполнитель или спам, агенты с участием человека в цикле дают наилучшее качество, а конкуренция между множеством агентов позволяет получить пригодный результат из 3-5 лучших заявок.
Anthropic убирает доступ к коду Claude из подписки Pro для новых пользователей в рамках теста.
Anthropic временно убрала доступ к Claude Code из своего плана подписки Pro за $20 в месяц для новых пользователей, изменив страницы с ценами на сайте и справочные документы, а затем отменив изменения. Компания описала это как 'небольшой тест для 2% новых подписок просьюмеров'.
Проект OT компании Meta: запланированное сокращение 60% команды с помощью ИИ отменено в последнюю минуту
Reuters раскрывает детали Project OT от Meta — плана по сокращению команд на 60% с помощью ИИ, который был отменён после протеста сотрудников. Тем не менее, команды столкнулись с сокращениями на 30-40%, а ключевые инженеры были переведены на разметку данных.