Запуск Palomar: реестр верифицированных доказательств на Lean

📌 Palomar - реестр проверенных LEAN-доказательств Последние месяцы доказательства, сгенерированные ИИ, посыпались валом как для новых результатов, так и для старых, причем часть из них формализована на Lean и проверить такой репозиторий непросто, особенно если ты не эксперт. Нужно убедиться: 🟠что заявленные формальные утверждения действительно имеют доказательства, проходящие проверку типов; 🟠что в доказательствах нет жульничества; 🟠что формальные утверждения по смыслу совпадают с тем, что описано словами. Под эту задачу и Теренс Тао запустил Palomar - реестр математики, верифицированной на Lean. Инициативу вырастили Lean FRO и ICARM. Прием заявок уже идет, чтобы в него попасть, в репозитории должно быть три вещи: 🟢challenge file с коротким и читаемым человеком описанием заявленных результатов на Lean; 🟢solution module с доказательством любой длины; 🟢файл formalization.yaml, где те же результаты изложены обычным языком и собраны метаданные и раскрытия. Снимок поданного репозитория проверяют двумя этапами. Сначала инструмент Comparator смотрит, что solution module типизируется и доказывает ровно то, что заявлено в challenge file. После этого языковая модель сверяет, похоже ли неформальное описание в на то, что заявлено формально. Прошел оба - попал в реестр. Принимают формализации и старых результатов, и новых. Кто автор доказательства - человек, ИИ или оба вместе - значения не имеет. @ai_machinelearning_big_data #news #ai #ml